diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-25 18:59:47 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-25 18:59:47 -0400 |
| commit | a31c716507d5373251dbd1ddfaf6f8e4f83d3a0a (patch) | |
| tree | fbfe62b1a82a5911ce36af82b0b1d5e7dc8a84da /folkwisdom.md | |
| parent | e61d477caa079526842d23a24aba4bdd9a2a8362 (diff) | |
s/fist/first/
Diffstat (limited to 'folkwisdom.md')
| -rw-r--r-- | folkwisdom.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/folkwisdom.md b/folkwisdom.md index a41d1532f..3530a517a 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -234,7 +234,7 @@ an abstract structure in multiple ways (e.g., integers can be a semiring under `+` and `*` or under `max` and `+`). Furthermore, we require that it be possible to manipulate abstractions using tactics. -To define an abstraction, fist open a module with no parameters to make a new +To define an abstraction, first open a module with no parameters to make a new namespace for the abstraction (even if the entire file is dedicated to one abstraction). Then open a new section and add to the context parameters for all definitions. The requirements which need to be satisfied by the definitions to |