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 ] Add equality as a parameter to Algebra.Consequences.Base #2572

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

[ refactor ] Add equality as a parameter to Algebra.Consequences.Base #2572

Changes from 1 commit
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
ff6f777
refactor: change top-level parameterisation, plus local `variable`s t…
jamesmckinna Feb 6, 2025
b920bef
refactor: propagate changes
jamesmckinna Feb 6, 2025
1e25c10
refactor: propagate changes; remove spurious anonymous modules
jamesmckinna Feb 6, 2025
6eab5f2
fix: `CHANGELOG`
jamesmckinna Feb 6, 2025
2433c3c
fix: deprecated names from #2206 / #2168
jamesmckinna Feb 6, 2025
d19dac9
fix: remove spurious blank line introduced by mistake
jamesmckinna Feb 6, 2025
075c94c
Merge branch 'agda:master' into issue2502-v2.3-equality
jamesmckinna Feb 19, 2025
0f720f8
fix: `CHANGELOG` entry
jamesmckinna Feb 19, 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
fix: deprecated names from #2206 / #2168
  • Loading branch information
@jamesmckinna
jamesmckinna committed Feb 6, 2025
commit 2433c3c7ac1154d7644e9cbcd8b1b75f958340e9
4 changes: 2 additions & 2 deletions src/Data/Rational/Unnormalised/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1144,7 +1144,7 @@ p≤q⇒0≤q-p {p} {q} p≤q = begin
*-zeroˡ p@record{} = *≡* refl

*-zeroʳ : RightZero _≃_ 0ℚᵘ _*_
*-zeroʳ = Consequences.comm+zeˡ⇒zeʳ ≃-setoid *-comm *-zeroˡ
*-zeroʳ = Consequences.comm∧zeˡ⇒zeʳ ≃-setoid *-comm *-zeroˡ

*-zero : Zero _≃_ 0ℚᵘ _*_
*-zero = *-zeroˡ , *-zeroʳ
Expand All @@ -1171,7 +1171,7 @@ invertible⇒≄ {p} {q} (1/p-q , 1/x*x≃1 , x*1/x≃1) p≃q = 0≄1 (begin
in *≡* eq where open ℤ-solver

*-distribʳ-+ : _DistributesOverʳ_ _≃_ _*_ _+_
*-distribʳ-+ = Consequences.comm+distrˡ⇒distrʳ ≃-setoid +-cong *-comm *-distribˡ-+
*-distribʳ-+ = Consequences.comm∧distrˡ⇒distrʳ ≃-setoid +-cong *-comm *-distribˡ-+

*-distrib-+ : _DistributesOver_ _≃_ _*_ _+_
*-distrib-+ = *-distribˡ-+ , *-distribʳ-+
Expand Down
Loading