agda/agda-stdlib

#2741

· jamesmckinna opened

on Jun 21, 2025

[Add] Consequences of associativity for `Semigroup`s

agda/agda-stdlib

#2688

· jmougeot opened

on Apr 1, 2025

· Changes requested

·

v2.3

· 12/12

81

[ refactor ] rationalise the common APIs for `List` and `Vec` versions of `Data..Relation.Binary.Lex.`

#2687

· jamesmckinna opened

on Mar 28, 2025

·

v3.0

Left/Right inconsistency

discussion

library-design

style-guide

#2654

· JacquesCarette opened

on Mar 12, 2025

1

Prefer `contradiction` over `⊥-elim` when it makes sense?

discussion

library-design

style-guide

#2653

· JacquesCarette opened

on Mar 11, 2025

13

Infix proofs

discussion

library-design

#2549

· JacquesCarette opened

on Jan 15, 2025

3

Refactor `Algebra.Consequences.*`?

discussion

library-design

refactoring

#2502

· jamesmckinna opened

on Nov 22, 2024

·

v3.0

6

Get rid of inconsistent `homo` name in algebra hierarchy?

breaking

discussion

naming

#2458

· jamesmckinna opened

on Aug 15, 2024

1

5

Linear-time implementation of `Data.Nat.Properties.≤′⇒≤`?

#2442

· jamesmckinna opened

on Jul 26, 2024

3

Proofs in `Data.Vec.Properties` take general properties as inputs

addition

discussion

library-design

#2421

· mildsunrise opened

on Jun 29, 2024

23

Rename `WeaklyDecidable`?

#2404

· jamesmckinna opened

on Jun 9, 2024

9

[DRY] what's the best way to `public`ly re-export properties/structure?

discussion

library-design

refactoring

#2391

· jamesmckinna opened

on May 20, 2024

6

Allow `.lagda` for library sources

discussion

documentation

library-design

#2379

· JacquesCarette opened

on May 3, 2024

9

To let or not to let

discussion

library-design

#2369

· JacquesCarette opened

on Apr 17, 2024

6

Add `Algebra.Action.*`

addition

discussion

library-design

#2348

· jamesmckinna opened

on Apr 8, 2024

1

10

What should our explicit import policy be?

discussion

library-design

#2339

· MatthewDaggitt opened

on Apr 1, 2024

10

Refactor `Data.List.Relation.Binary.Permutation.*`

agda/agda-stdlib

#2317

· jamesmckinna opened

on Mar 12, 2024

· Review required

13

Add `List.Base.build`/Church encodings of `Data` types

addition

discussion

library-design

#2304

· jamesmckinna opened

on Feb 27, 2024

Modular arithmetic based on `Data.Nat.Bounded` #2257

addition

discussion

library-design

agda/agda-stdlib

#2292

· jamesmckinna opened

on Feb 12, 2024

· Review required

· 2/2

5

Streamlining the `make test`/CI infrastructure?

admin

continuous-integration

discussion

#2248

· jamesmckinna opened

on Jan 4, 2024

3

Relations in proofs in `Data.Product.Relation.Binary.Pointwise.NonDependent` don't appear to be inferable

#2174

· MatthewDaggitt opened

on Oct 20, 2023

3

Naming inversion principles for (one-constructor) `data`types

#2155

· jamesmckinna opened

on Oct 16, 2023

9

Refactoring uses of `with`

discussion

library-design

refactoring

#2123

· jamesmckinna opened

on Oct 5, 2023

Reconciling `Data.Nat.Divisibility.Core._∣_` and `Algebra.Definitions.RawMagma._∣_`

#2115

· jamesmckinna opened

on Sep 29, 2023

·

v3.0

17

The free `Magma` on a `Set`, resp. `Setoid` [bis]

status: blocked-by-issue

agda/agda-stdlib

#1962

· jamesmckinna opened

on May 1, 2023

· Approved

63

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[ deprecate ] `Relation.Nullary.Reflects` and [ refactor ] `Relation.Nullary.Decidable.Core`

[Add] Consequences of associativity for `Semigroup`s

[ refactor ] rationalise the common APIs for `List` and `Vec` versions of `Data..Relation.Binary.Lex.`

Left/Right inconsistency

Prefer `contradiction` over `⊥-elim` when it makes sense?

Infix proofs

Refactor `Algebra.Consequences.*`?

Get rid of inconsistent `homo` name in algebra hierarchy?

Linear-time implementation of `Data.Nat.Properties.≤′⇒≤`?

Proofs in `Data.Vec.Properties` take general properties as inputs

Rename `WeaklyDecidable`?

[DRY] what's the best way to `public`ly re-export properties/structure?

Allow `.lagda` for library sources

To let or not to let

Add `Algebra.Action.*`

What should our explicit import policy be?

Refactor `Data.List.Relation.Binary.Permutation.*`

Add `List.Base.build`/Church encodings of `Data` types

Modular arithmetic based on `Data.Nat.Bounded` #2257

Streamlining the `make test`/CI infrastructure?

Relations in proofs in `Data.Product.Relation.Binary.Pointwise.NonDependent` don't appear to be inferable

Naming inversion principles for (one-constructor) `data`types

Refactoring uses of `with`

Reconciling `Data.Nat.Divisibility.Core._∣_` and `Algebra.Definitions.RawMagma._∣_`

The free `Magma` on a `Set`, resp. `Setoid` [bis]

Issues

Search results