Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[ refactor ] (Re)define (Is)TightApartness and (Is)HeytingCommutativeRing/(Is)HeytingField #2588

Open
wants to merge 16 commits into
base: master
Choose a base branch
from
Open

[ refactor ] (Re)define (Is)TightApartness and (Is)HeytingCommutativeRing/(Is)HeytingField #2588

Changes from 1 commit
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
d171042
refactor: fix #2587
jamesmckinna Feb 18, 2025
d07718c
refactor: properties of `HeytingField`, not `HeytingCommutativeRing`
jamesmckinna Feb 18, 2025
7f2f4af
refactor: give `DecSetoid`s the structure of `(Is)TightApartnessRelat…
jamesmckinna Feb 18, 2025
408433d
fix: unsaved commits
jamesmckinna Feb 18, 2025
92f8248
refactor: move property `x-0≈x` to `Algebra.Properties.AbelianGroup`,…
jamesmckinna Feb 19, 2025
55a7384
refactor: deprecate and tighten `import`s
jamesmckinna Feb 19, 2025
3786f55
fix: `CHANGELOG` plus tidying up
jamesmckinna Feb 19, 2025
5da81d0
Merge branch 'master' into refactor-heyting
jamesmckinna Feb 19, 2025
31b51a6
refactor: resolve merge of #2576
jamesmckinna Feb 19, 2025
f891093
refactor: another attempt to resolve merge of #2576
jamesmckinna Feb 19, 2025
a8d6284
refactor: re-export from `Relation.Binary.Properties.(Dec)Setoid`
jamesmckinna Feb 19, 2025
1f9a4c1
refactor: tighten re-export from `Relation.Binary.Properties.DecSetoid`
jamesmckinna Feb 19, 2025
48bef4a
refactor: re-export from `apartnessRelation` from `HeytingCommutative…
jamesmckinna Feb 19, 2025
cdc57d2
fix: better `CHANGELOG`?
jamesmckinna Feb 19, 2025
fb2da3e
fix: one last re-export?
jamesmckinna Feb 19, 2025
8dcb5b6
Merge branch 'agda:master' into refactor-heyting
jamesmckinna Feb 21, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
refactor: tighten re-export from Relation.Binary.Properties.DecSetoid
  • Loading branch information
@jamesmckinna
jamesmckinna committed Feb 19, 2025
commit 1f9a4c18d75f8889ac1bdb6310fd219d1776354c
2 changes: 1 addition & 1 deletion src/Data/Rational/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1279,7 +1279,7 @@ module _ where
using (+-group; zeroˡ; *-congʳ; isCommutativeRing)

open GroupProperties +-group
open DecSetoidProperties ≡-decSetoid
open DecSetoidProperties ≡-decSetoid using (≉-isTightApartnessRelation)

#⇒invertible : p ≢ q → Invertible 1ℚ _*_ (p - q)
#⇒invertible {p} {q} p≢q = let r = p - q in 1/ r , *-inverseˡ r , *-inverseʳ r
Expand Down
Loading