From a31c716507d5373251dbd1ddfaf6f8e4f83d3a0a Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 18:59:47 -0400 Subject: s/fist/first/ --- folkwisdom.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'folkwisdom.md') 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 -- cgit v1.2.3