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:42] dave [Standard Library] |
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 = 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 120: | Line 120: | ||
| * If ''n'' is a ''nat'', then the expression ''S n'' is the same as ''n + 1''. | * 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 *very* weird.) | + | * 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''. | * S is one of the constructors of ''nat'' which takes a single argument having type ''nat''. | ||
math/coq_notes.1549233731.txt.gz · Last modified: 2019/02/03 14:42 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
