'No infinite descent' for (`Acc`essible elements of) `WellFounded` relations#2126

Merged

MatthewDaggitt merged 64 commits intoagda:masterfrom

jamesmckinna:NoInfiniteDescent

Mar 16, 2024

Commits on Oct 8, 2023

Commits on Oct 9, 2023

Commits on Nov 4, 2023

[fixes #2130] Moving `Properties.HeytingAlgebra` from `Relation.Binary` to `Relation.Binary.Lattice` (#2131)
jamesmckinna
committed
[fixes #2127] Fixes #1930 `import` bug (#2128)
jamesmckinna
committed
[fixes #1214] Add negated ordering relation symbols systematically to `Relation.Binary.*` (#2095)
jamesmckinna
committed
Refactoring (inversion) properties of `_<_` on `Nat`, plus consequences (#2000)
jamesmckinna
committed
Bump CI tests to Agda-2.6.4 (#2134)

MatthewDaggitt
authored and
jamesmckinna
committed
Remove `Algebra.Ordered` (#2133)

MatthewDaggitt
authored and
jamesmckinna
committed
[ fix ] missing name in LICENCE file (#2139)

gallais
authored and
jamesmckinna
committed
Add new blocking primitives to `Reflection.TCM` (#1972)

plt-amy
authored and
jamesmckinna
committed
Change definition of `IsStrictTotalOrder` (#2137)

MatthewDaggitt
authored and
jamesmckinna
committed
Add _<$>_ operator for Function bundle (#2144)

MatthewDaggitt
authored and
jamesmckinna
committed
[ fix #2086 ] new web deployment strategy (#2147)

gallais
authored and
jamesmckinna
committed
[ admin ] fix sorting logic (#2151)

gallais
authored and
jamesmckinna
committed
Add coincidence law to modules (#1898)

Taneb
authored and
jamesmckinna
committed
Make reasoning modular by adding new `Reasoning.Syntax` module (#2152)

MatthewDaggitt
authored and
jamesmckinna
committed
Fixes typos identified in #2154 (#2158)
jamesmckinna
committed
tackles #2124 as regards `case_return_of_` (#2157)
jamesmckinna
committed
Rename preorder ~ relation reasoning combinators (#2156)

MatthewDaggitt
authored and
jamesmckinna
committed
Move ≡-Reasoning from Core to Properties and implement using syntax (#2159)

MatthewDaggitt
authored and
jamesmckinna
committed
Add consistent deprecation warnings to old function hierarchy (#2163)

MatthewDaggitt
authored and
jamesmckinna
committed
Rename symmetric reasoning combinators. Minimal set of changes (#2160)

MatthewDaggitt
authored and
jamesmckinna
committed
Restore 'return' as an alias for 'pure' (#2164)

MatthewDaggitt
authored and
jamesmckinna
committed
[ fix #2153 ] Properly re-export specialised combinators (#2161)

gallais
authored and
jamesmckinna
committed
Connect `LeftInverse` with (`Split`)`Surjection` (#2054)

laMudri
authored and
jamesmckinna
committed
Added remaining flipped and negated relations to binary relation bundles (#2162)

MatthewDaggitt
authored and
jamesmckinna
committed
Tidy up CHANGELOG in preparation for release candidate (#2165)

MatthewDaggitt
authored and
jamesmckinna
committed
Spellcheck CHANGELOG (#2167)
jamesmckinna
committed
Fixed Agda version typo in README (#2176)
jamesmckinna
committed
Fixed in deprecation warning for `<-transˡ` (#2173)
jamesmckinna
committed
Bump Haskell CI (original!) to latest minor GHC versions (#2187)

andreasabel
authored and
jamesmckinna
committed
[fixes #2175] Documentation misc. typos etc. for RC1 (#2183)

jamesmckinna
and
MatthewDaggitt
committed
[fixes #2178] regularise and specify/systematise, the conventions for symbol usage (#2185)
jamesmckinna
committed
Move `T?` to `Relation.Nullary.Decidable.Core` (#2189)

MatthewDaggitt
authored and
jamesmckinna
committed
Make decidable versions of sublist functions the default (#2186)

MatthewDaggitt
authored and
jamesmckinna
committed
Merge branch 'master' into NoInfiniteDescent
jamesmckinna
authored

Commits on Dec 14, 2023

Commits on Dec 17, 2023

Commits on Dec 31, 2023

Commits on Jan 31, 2024

Merge branch 'master' into NoInfiniteDescent
jamesmckinna
authored

Commits on Feb 26, 2024

cosmetics asper final comment
jamesmckinna
committed

Commits on Mar 16, 2024

Merge branch 'master' into NoInfiniteDescent
MatthewDaggitt
authored