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
+5-5Lines changed: 5 additions & 5 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -100,7 +100,7 @@ We present the Agda standard library [@agda-stdlib-v2.0] (`agda-stdlib`), which
100
100
101
101
Besides providing common utilities and data structures, `agda-stdlib` is especially necessary compared to standard libraries for traditional languages for two reasons.
102
102
103
-
First, Agda is a small, powerful language that omits concepts usually built-in to a language (e.g. numbers, strings).
103
+
First, Agda is a small, powerful language that omits concepts usually built-in to a language (e.g., numbers, strings).
104
104
This reduces compiler complexity, but leaves `agda-stdlib` to define them.
105
105
106
106
Second, functions in `agda-stdlib` come with correctness proofs - these require substantial work that should not fall to users.
@@ -123,7 +123,7 @@ A diverse set of verification projects use `agda-stdlib`, including:
123
123
124
124
The library has had a synergistic relationship with Agda itself, both testing and motivating new language features.
125
125
For example, since Agda supports many incompatible language extensions, `agda-stdlib` is structured modularly to remain compatible with different combinations of extensions.
126
-
Each module requests only the minimal expressive power it needs and to facilitate this Agda now categorises extensions as "infective" (affecting all import*ing* modules), "coinfective" (affecting all import*ed* modules) or "neither".
126
+
Each module requests only the minimal expressive power it needs and to facilitate this Agda now categorises extensions as "infective" (affecting all import*ing* modules), "coinfective" (affecting all import*ed* modules), or "neither".
127
127
The library has also served as a test bed for alternative approaches to defining co-inductive data types in Agda.
128
128
129
129
# Design
@@ -141,7 +141,7 @@ To our knowledge, `agda-stdlib` is among the first ITP standard libraries to who
141
141
142
142
In contrast to the type-class mechanisms often used by other functional languages, `agda-stdlib` primarily supports polymorphism [@ivardeBruin2023] via extensive use of parametrised modules.
143
143
This allows users to specify instantiations of abstract parameters for whole modules in a single location, reducing the need for instance search.
144
-
A drawback is imports must be qualified when code is instantiated multiple times in the same scope.
144
+
A drawback is that imports must be qualified when code is instantiated multiple times in the same scope.
145
145
Parameterised modules are also used to safely and scalably embed non-constructive mathematics into a constructive setting.
146
146
147
147
The README directory within the library contains both documentation on the general design decisions and
@@ -159,7 +159,7 @@ Version 2.0 of `agda-stdlib` [@agda-stdlib-v2.0] has attempted to address some o
159
159
160
160
- Minimised Dependency Graphs: core modules rely on fewer parts of the library, resulting in faster load times.
161
161
162
-
- Standardisation: mathematical objects and their morphisms (e.g. groups, rings) are now constructed more uniformly, enhancing consistency and usability.
162
+
- Standardisation: mathematical objects and their morphisms (e.g., groups, rings) are now constructed more uniformly, enhancing consistency and usability.
163
163
164
164
- Tactics Library: expanded the set of available tactics (although performance can still be improved).
165
165
@@ -169,7 +169,7 @@ Version 2.0 of `agda-stdlib` [@agda-stdlib-v2.0] has attempted to address some o
169
169
170
170
Nils Anders Danielsson provided substantial feedback.
171
171
172
-
Authors are listed approximately in order of contribution. Manuscript by Daggitt, Allais, McKinna, Carette and van Doorn. A list of all contributors is available on GitHub.
172
+
Authors are listed approximately in order of contribution. Manuscript by Daggitt, Allais, McKinna, Carette, and van Doorn. A list of all contributors is available on GitHub.
0 commit comments