agda/agda-stdlib

Issues

• Unsolved metas in `Data.List.Properties` cf. discussion on #2415, #2359, #2365

  #2427 opened 6 months ago by jamesmckinna
  5

• Update installation instructions wrt install dir?

  #2500 opened a month ago by jbclements
  2

• Are `Irrelevant` types `Recomputable`?

  #2495 opened 2 months ago by jamesmckinna
  2

• Problem with `DISPLAY` pragma for `⊥` in `Data.Empty`

  #2493 opened 3 months ago by jamesmckinna
  6

• Missing structure/bundle in the `Relation.Binary.*` hierarchy?

  #2482 opened 3 months ago by jamesmckinna
  3

• Runtime irrelevance

  #2486 opened 3 months ago by kurnevsky
  7

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

  #2391 opened 7 months ago by jamesmckinna
  6

• [DRY] Refactor algebraic properties of types

  #2489 opened 3 months ago by jamesmckinna
  0

• Equivalence of characterisations of `Data.List.Membership.Setoid._∉_`

  #2466 opened 3 months ago by jamesmckinna
  1

• Add `EquationalReasoning` combinators for `_∼[ set ]_`?

  #2483 opened 3 months ago by jamesmckinna
  2

• [DRY?] Direct definition vs. generic combinators, ctd. in `Algebra.Definitions.RawMonoid`

  #2475 opened 4 months ago by jamesmckinna
  3

• two proofs suggested for `Data.List.Membership.Setoid.Properties`

  #2463 opened 4 months ago by mechvel
  2

• Release v2.1.1

  #2461 opened 4 months ago by JacquesCarette
  22

• Find all single letter publicly-exported modules and make sure they are private

  #2472 opened 4 months ago by MatthewDaggitt
  5

• `Relation.Binary.Definitions._Respects₂_` seems to exchange 'left' and 'right' in its left/right projections?

  #2471 opened 4 months ago by jamesmckinna
  2

• somethig like a typo in lib-2.1.1-rc2

  #2467 opened 4 months ago by mechvel
  5

• [DRY] Refactor `Algebra.Solver.*Monoid` (or deprecate entirely?)

  #2403 opened 4 months ago by jamesmckinna
  0

• Data.Nat.Properties.≤-total should be implemented with _<ᵇ_

  #2436 opened 5 months ago by Taneb
  14

• Add `Algebra.Definitions.RawGroup` and `Algebra.Properties.Group.*`

  #2454 opened 5 months ago by jamesmckinna
  5

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

  #2458 opened 4 months ago by jamesmckinna
  5

• Reflection.AST.Definition doesn't compile in release candidate

  #2462 opened 4 months ago by alexarice
  6

• Derived operators in the theory of `Relation.Binary.Structures.IsTotalOrder`

  #2448 opened 4 months ago by jamesmckinna
  5

• [DRY] Refactor the various definitions of 'pointwise' equality on functions/`Function`s/pointwise `Algebra`s

  #2434 opened 6 months ago by jamesmckinna
  2

• Add `Algebra.Properties.IdempotentCommutativeMonoid`

  #2408 opened 5 months ago by jamesmckinna
  0

• To let or not to let

  #2369 opened 8 months ago by JacquesCarette
  6

• Deploy doc rendering for v2.1

  #2452 opened 5 months ago by andreasabel
  2

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

  #2442 opened 5 months ago by jamesmckinna
  3

• Refactor ` Data.Nat.GeneralisedArithmetic`

  #2446 opened 5 months ago by jamesmckinna
  2

• Regression in the documentation of installation

  #2443 opened 5 months ago by gallais
  1

• Data.List.upTo/applyUpTo can be made faster

  #2437 opened 5 months ago by Taneb
  5

• Style for lower/upper case for initial letter in denotations

  #2417 opened 6 months ago by mechvel
  7

• Unify general algebraic definitions of Divisibility and Primarity with those in Nat and Integer

  #2416 opened 5 months ago by mechvel
  7

• What's the 'right' notion of equality between functions?

  #2400 opened 6 months ago by jamesmckinna
  7

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

  #2421 opened 6 months ago by mildsunrise
  23

• List of sub-optimal definitions in `Data.List.Base`

  #2359 opened 8 months ago by JacquesCarette
  28

• comments on lib-2.1 candidate 1

  #2415 opened 6 months ago by mechvel
  9

• Restore missing proofs from `Algebra.Operations.CommutativeMonoid`

  #2420 opened 6 months ago by jamesmckinna
  0

• Naming of new functions `tail∘inits` and `tail∘tails`

  #2411 opened 6 months ago by MatthewDaggitt
  5

• Rename `WeaklyDecidable`?

  #2404 opened 6 months ago by jamesmckinna
  4

• Why is `Data.List.Relation.Binary.Subset.Setoid.Properties` not parametrized on the `Setoid` as a whole

  #2397 opened 7 months ago by andreasabel
  5

• Use the Monoid structure of Endomorphisms to define powering

  #2394 opened 7 months ago by JacquesCarette
  1

• Add the `Setoid`al structure of a (free) `Monoid` on `List`

  #2360 opened 7 months ago by jamesmckinna
  1

• Document `variable` block indentation style

  #2390 opened 7 months ago by JacquesCarette
  5

• [DRY] More redundant `zero` fields in `Algebra.Structures`

  #2396 opened 7 months ago by jamesmckinna
  0

• Add bundled mono-/iso-{/epi-} morphisms

  #2387 opened 7 months ago by jamesmckinna
  0

• Add bundles for lattice-like and module-like morphisms

  #2388 opened 7 months ago by jamesmckinna
  0

• lemma for `map` for `⊆` as Subset

  #2375 opened 7 months ago by mechvel
  0

• Allow `.lagda` for library sources

  #2379 opened 8 months ago by JacquesCarette
  7

• `m+[n∸m]≡n` in the wrong section

  #2384 opened 8 months ago by gallais
  2

• lib2.0 : `ℕᵇ `(binary) can be pure unlike `ℕ`.

  #2362 opened 8 months ago by mechvel
  8