[ refactor ] make n≢i : n ≢ toℕ i argument to lower₁ irrelevant#2783
Open
jamesmckinna wants to merge 8 commits intoagda:masterfrom
Open
[ refactor ] make `n≢i : n ≢ toℕ i` argument to `lower₁` irrelevant#2783jamesmckinna wants to merge 8 commits intoagda:masterfrom
jamesmckinna wants to merge 8 commits intoagda:masterfrom
Commits
Commits on Jul 25, 2025
Commits on Jul 26, 2025
Commits on Jul 27, 2025
- committed