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
+4-3Lines changed: 4 additions & 3 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -47,7 +47,8 @@ authors:
47
47
orcid: 0000-0003-2673-4400
48
48
affiliation: 12
49
49
- name: You, Shu-Hung
50
-
affiliation: 12
50
+
orcid: 0009-0003-0003-3945
51
+
affiliation: 13
51
52
- name: Mullanix, Reed
52
53
orcid: 0000-0002-7970-4961
53
54
affiliation: 9
@@ -159,7 +160,7 @@ On the other hand, `batteries` and `mathlib` [@van2020maintaining] for Lean prov
159
160
Philosophically, `agda-stdlib` is more closely aligned with the approach of the MathLib library, and our aim is to provide canonical definitions for mathematical objects and introduce new representations only sparingly.
160
161
161
162
A second challenge is that `agda-stdlib` has embraced the "intrinsic style" of dependent types, in which correctness-related invariants are part of data structures, rather than separate predicates.
162
-
Many definitions in agda-stdlib use this intrinsic style.
163
+
Many definitions in `agda-stdlib` use this intrinsic style.
163
164
For instance, the final definition of rational numbers is a record type that alongside the numerator and denominator contains a proof showing that the numerator and denominator have no common factors.
164
165
The intrinsic style also includes returning proofs rather than, say, booleans from decision procedures.
165
166
The standard library for instance uses this approach for its implementation of regular expression matching which along with the match returns a proof justifying it.
@@ -208,7 +209,7 @@ The authors of this paper are listed approximately in order of contribution to t
208
209
# Funding and conflicts of interest
209
210
210
211
The authors of this paper have no conflicts of interest to declare.
211
-
Many of the contributions to the library by the authors of this paper were made over a significant period of time and while at other institutions than their current affliation. Some of the contributions have been made while receiving funding for related projects, and a non-exhaustive list of such funding follows:
212
+
Many of the contributions to the library by the authors of this paper were made over a significant period of time and while at other institutions than their current affiliation. Some of the contributions have been made while receiving funding for related projects, and a non-exhaustive list of such funding follows:
212
213
213
214
- Jason Z. S. Hu made his contributions during his funded Master's and PhD study.
0 commit comments