You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: paper/paper.md
+2-2Lines changed: 2 additions & 2 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -129,10 +129,10 @@ The library has also served as a test bed for alternative approaches to defining
129
129
# Design
130
130
131
131
Organising libraries of discrete mathematics and algebra coherently is notoriously difficult
132
-
[@carette2020leveraging][@cohen2020hierarchy].
132
+
[@carette2020leveraging; @cohen2020hierarchy].
133
133
There is a tension between maximising generality and providing direct, intuitive definitions.
134
134
Mathematical objects often admit multiple representations with different benefits, but this leads to redundancy.
135
-
Some ITPs ([@coq2024manual], [@paulson1994isabelle]) have a rich ecosystem of external libraries, avoiding canonical definitions at the cost of incompatibilities.
135
+
Some ITPs ([@coq2024manual; @paulson1994isabelle]) have a rich ecosystem of external libraries, avoiding canonical definitions at the cost of incompatibilities.
136
136
We have chosen, like Lean's `mathlib`[@van2020maintaining], to provide a repository of canonical definitions.
137
137
138
138
`agda-stdlib` adopts the "intrinsic style" of dependent types, where data structures themselves contain correctness invariants.
0 commit comments