math:coq_notes
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
math:coq_notes [2019/02/03 14:42] dave [Oddities] |
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" | ||
math/coq_notes.1549233766.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
