Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Sep 2, 2025

• Merge remote-tracking branch 'Taneb/reals'

  glittershark

  committed
  f94a3c8

  Copy full SHA for f94a3c8

Commits on Aug 6, 2025

• [ add ] `style-guide` recommendation preferring `contradiction` over `⊥-elim` (#2798)

  Show description for 54f5c38
  

  jamesmckinna

  and

  JacquesCarette

  authored
  54f5c38

  Copy full SHA for 54f5c38

Commits on Aug 5, 2025

• [Add] padRight properties to Data.Vec.Properties (#2769)

  Show description for 08bc2b8
  

  e-mniang

  and

  jamesmckinna

  authored
  08bc2b8

  Copy full SHA for 08bc2b8

• [ add ] eta law for ¬¬ monad (#2803)

  Show description for 3337e54
  jamesmckinna

  authored
  3337e54

  Copy full SHA for 3337e54

Commits on Aug 2, 2025

• Backport changes from 2.3 release to 2.4 (#2799)

  Show description for f767c72
  

  5 peopleauthored
  f767c72

  Copy full SHA for f767c72

• [ fix ] release guide (#2800)

  jamesmckinna

  authored
  84f1ab2

  Copy full SHA for 84f1ab2

• [ refactor ] `Data.Fin.Properties` of decidable equality, plus knock-ons (#2740)

  Show description for d4c0a97
  jamesmckinna

  authored
  d4c0a97

  Copy full SHA for d4c0a97

• refactor: weaken type of `contradiction-irr` (#2785)

  jamesmckinna

  authored
  35396e4

  Copy full SHA for 35396e4

Commits on Jul 31, 2025

• [ add ] commentary explaining the `IsXRing` design problem (issues #1617 and #2771) (#2781)

  Show description for 0fa3e60
  jamesmckinna

  authored
  0fa3e60

  Copy full SHA for 0fa3e60

• [ add ] rule of signs for `RingWithoutOne` (#2761)

  Show description for 276ca7e
  jamesmckinna

  authored
  276ca7e

  Copy full SHA for 276ca7e

• [ DRY ] redefine `Algebra.Definitions.Medial` in terms of `Interchangable` (#2764)

  Show description for 604b1f4
  jamesmckinna

  authored
  604b1f4

  Copy full SHA for 604b1f4

• [ add ] Choudhury and Fiore's alternative definition of `Permutation` for `Setoid`s (#2726)

  Show description for aef1785
  jamesmckinna

  authored
  aef1785

  Copy full SHA for aef1785

Commits on Jul 28, 2025

• [ add ] `∸-suc` lemma for natural numbers (#2757)

  Show description for aab6732
  

  pmbittner

  and

  jamesmckinna

  authored
  aab6732

  Copy full SHA for aab6732

• [fix]: error in README.Data.Fin.Relation.Unary.Top (#2791)

  pmbittner

  authored
  628f0a2

  Copy full SHA for 628f0a2

Commits on Jul 20, 2025

• reset `stdlib` for v2.4 (#2775)

  Show description for 0e97e2e
  jamesmckinna

  authored
  0e97e2e

  Copy full SHA for 0e97e2e

Commits on Jul 18, 2025

• Refactor CHANGELOG in preparation for v2.3-rc1 (#2773)

  Show description for 15a6bbe
  

  MatthewDaggitt

  and

  jamesmckinna

  authored
  15a6bbe

  Copy full SHA for 15a6bbe

• Fix breaking introduction of variable (#2774)

  MatthewDaggitt

  authored
  1029995

  Copy full SHA for 1029995

Commits on Jul 17, 2025

• [ DRY ] refactor `Algebra.Properties.{Quasigroup|Loop}` (#2768)

  Show description for ba505b0
  jamesmckinna

  authored
  ba505b0

  Copy full SHA for ba505b0

• Add instances of `IsString (List Char)` (#2756)

  Show description for eef9345
  rvs314

  authored
  eef9345

  Copy full SHA for eef9345

• [Add] Consequences of identity for `monoids` (#2692)

  Show description for 7367bae
  

  3 peopleauthored
  7367bae

  Copy full SHA for 7367bae

Commits on Jul 11, 2025

• refactor: cosmetic improvement over #2546 (#2759)

  jamesmckinna

  authored
  5c64117

  Copy full SHA for 5c64117

Commits on Jul 3, 2025

• Delete rewrite steps that do not fire (#2758)

  Show description for 6f8af94
  andreasabel

  authored
  6f8af94

  Copy full SHA for 6f8af94

• [ refactor ] Restate, and use, the definitions of `Monotonic` etc. operations (#2580)

  Show description for b58fc90
  

  jamesmckinna

  and

  MatthewDaggitt

  authored
  b58fc90

  Copy full SHA for b58fc90

Commits on Jul 2, 2025

• [Add] Consequences of associativity for `Semigroup`s (#2688)

  Show description for 77fed0b
  

  jmougeot

  and

  jamesmckinna

  authored
  77fed0b

  Copy full SHA for 77fed0b

• Lemmata for `if_then_else_` (#2747)

  Show description for 327ec79
  pmbittner

  authored
  327ec79

  Copy full SHA for 327ec79

• Proved sorted permutations are equal (#2748)

  Show description for 5bd195e
  MatthewDaggitt

  authored
  5bd195e

  Copy full SHA for 5bd195e

• Adds Algebra.Morphism.Construct.DirectProduct (#2715)

  Show description for ebe659c
  carlostome

  authored
  ebe659c

  Copy full SHA for ebe659c

Commits on Jun 30, 2025

• Refactor `Data.Vec.Properties` : Add toList-injective and new lemmas (#2733)

  Show description for a53588f
  

  jmougeot

  and

  MatthewDaggitt

  authored
  a53588f

  Copy full SHA for a53588f

• added insertion sort and refactored merge sort (#2751)

  Show description for c645989
  onestruggler

  authored
  c645989

  Copy full SHA for c645989

• Switch to Agda 2.8.0-rc3 by merging `experimental` into `master` (#2755)

  Show description for b6feb45
  

  MatthewDaggitt

  and

  andreasabel

  authored
  b6feb45

  Copy full SHA for b6feb45

• [ add ] `Relation.Nullary.Decidable.dec-yes-recompute` (#2738)

  Show description for fe7e88e
  jamesmckinna

  authored
  fe7e88e

  Copy full SHA for fe7e88e

• Some extra support for homogeneous n-ary products (#2736)

  Show description for 915d81c
  

  MatthewDaggitt

  and

  jamesmckinna

  authored
  915d81c

  Copy full SHA for 915d81c

Commits on Jun 27, 2025

• fix: #2752 (#2753)

  jamesmckinna

  authored
  2d5732c

  Copy full SHA for 2d5732c

Commits on Jun 26, 2025

• Adds unary disjoint relation (#2595)

  Show description for 29d1632
  

  3 peopleauthored
  29d1632

  Copy full SHA for 29d1632

Commits on Jun 25, 2025

• Some preparatory proofs for proving sorting+permutation is equality #2724 (#2725)

  Show description for f5e4c2b
  

  MatthewDaggitt

  and

  jamesmckinna

  authored
  f5e4c2b

  Copy full SHA for f5e4c2b

Pagination

Previous

Next