merging informal description with bnf

2017-07-14 11:02:44 +01:00 · 2017-07-14 11:02:44 +01:00 · 626d87804f
commit 626d87804f
parent 5b63add070
3 changed files with 2884 additions and 2876 deletions
--- a/out/Stlc.md
+++ b/out/Stlc.md
--- a/out/StlcProp.md
+++ b/out/StlcProp.md
--- a/src/Stlc.lagda
+++ b/src/Stlc.lagda
@ -57,7 +57,9 @@ numbers as a base type.

 Here is the syntax of types in BNF.

-    A, B, C ::= A ⇒ B | 𝔹
+    A, B, C ::=
+      A ⇒ B   -- functions
+      𝔹        -- booleans

 And here it is formalised in Agda.

@ -89,6 +91,8 @@ correspond to introduction rules and deconstructors to eliminators.

 Here is the syntax of terms in BNF.

+    L, M, N ::= ` x | λ[ x ∶ A ] N 
+