math:coq_notes
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
math:coq_notes [2019/02/03 14:35] dave [Vernacular Commands] |
math:coq_notes [2019/02/03 19:44] (current) dave [Vernacular Commands] |
||
|---|---|---|---|
| Line 82: | Line 82: | ||
| Theorem <test_name>: [<quantifier>,] <boolean expression>. | Theorem <test_name>: [<quantifier>,] <boolean expression>. | ||
| </code> | </code> | ||
| - | * Example of a quantifier: ''for all: n:nat'':<code> | + | * Example of a quantifier: ''forall n:nat'':<code> |
| - | Theorem n_plus_0 : forall: n:nat, 0 + n = S n. | + | Theorem n_plus_0 : forall n:nat, 0 + n = n. |
| </code> | </code> | ||
| * The above simply states: "Adding zero to every natural number results in the same natural number" | * The above simply states: "Adding zero to every natural number results in the same natural number" | ||
| Line 117: | Line 117: | ||
| [[https://coq.inria.fr/refman/coq-tacindex.html|Tactic Index]] | [[https://coq.inria.fr/refman/coq-tacindex.html|Tactic Index]] | ||
| + | ===== Oddities == | ||
| + | |||
| + | * If ''n'' is a ''nat'', then the expression ''S n'' is the same as ''n + 1''. | ||
| + | * This is because ''nat'' modeled as a linked list with no item--the value is encoded in the number of links in the list. (This is a *very* weird way to model numbers.) | ||
| + | * S is one of the constructors of ''nat'' which takes a single argument having type ''nat''. | ||
| + | |||
| + | |||
| ===== Standard Library == | ===== Standard Library == | ||
math/coq_notes.1549233303.txt.gz · Last modified: 2019/02/03 14:35 by dave
Page Tools
Except where otherwise noted, content on this wiki is licensed under the following license: CC Attribution-Noncommercial-Share Alike 4.0 International
