Michael Gilliland
696f336096
Replace "metavariable" with "hole"
2015-06-30 20:37:17 -04:00
Edwin Brady
61870cb9b2
Change wording in unification errors
...
"Can't unify" and "Can't convert" are terrible error messages for
programmers, and particularly confusing to explain to beginners, because
programmers don't need to know that implementation detail.
Changed to "type mismatch" and updated docs accordingly.
2015-05-24 23:23:20 +01:00
Maxim Ivanov
21309686a7
minor editorials
...
- fix section crosslink
- terminate sentence with a dot rather than comma
2015-05-09 00:57:31 +07:00
Jan de Muijnck-Hughes
87039fb0a7
Heading normalisation, and reST usage fixes.
...
+ Fixed minor reST inconsistencies.
+ Normalised syntax used for headers to become inline with the [convention used for Python](http://sphinx.readthedocs.org/en/latest/rest.html#sections )
2015-03-31 09:47:59 +01:00
Edwin Brady
029413ba8a
Typo fix
2015-03-30 09:19:18 +01:00
Edwin Brady
035f24e4e7
Move tactic proofs out of main tutorial
...
Also add a note that this is not intended to be used directly, but
rather for building proof automation
2015-03-30 09:17:49 +01:00
bmastenbrook
df1af5ff99
Fix some missing words
2015-03-23 18:47:51 -05:00
bmastenbrook
04831cf0bd
Fix some minor typos
2015-03-23 18:39:25 -05:00
Edwin Brady
f5aea0052e
Move total annotation in proof description
2015-03-23 23:26:28 +00:00
Edwin Brady
0621bdc6d1
More typos in theorem proving tutorial
2015-03-23 23:21:50 +00:00
Edwin Brady
142f92f387
Fix some pandoc conversion errors
2015-03-23 23:12:35 +00:00
Edwin Brady
9f4aea3bfa
Correct error message in proof docs
2015-03-23 23:04:10 +00:00
Edwin Brady
be93168682
Add section on theorem proving to tutorial
2015-03-23 23:00:58 +00:00
