diff options
Diffstat (limited to 'content/zettel/3b2.md')
| -rw-r--r-- | content/zettel/3b2.md | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/content/zettel/3b2.md b/content/zettel/3b2.md new file mode 100644 index 0000000..387ac8a --- /dev/null +++ b/content/zettel/3b2.md @@ -0,0 +1,17 @@ ++++ +title = "Stack Machine" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3b1"] +forwardlinks = ["3b3"] +zettelid = "3b2" ++++ + +The theoretical foundation of Coq is called Calculus of Inductive +Constructions (CIC), an extension to the older Calculus of Construction +(CoC). Gallina is actually an extension of CIC which is all the code +that comes after the `:=` and before the period. Next there is LTac, +which is a domain-specific language for writing proofs and decision +procedures. Finally, commands like `Inductive` and `Definition` are the +Vernacular, which supports many queries to the Coq system. |