Mercurial > cpdt > repo

comparison src/Match.v @ 301:f4768d5a75eb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Typo fix
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Jan 2011 11:42:09 -0500
parents b441010125d4
children 7b38729be069
comparison
equal deleted inserted replaced
300:25ec92be5ad2 301:f4768d5a75eb
542 ============================ 542 ============================
543 False 543 False
544 544
545 ]] 545 ]]
546 546
547 We use the [pose] tactic, which extends the proof context with a new variable that is set equal to particular a term. We could also have used [idtac n] in place of [pose n], which would have printed the result without changing the context. 547 We use the [pose] tactic, which extends the proof context with a new variable that is set equal to a particular term. We could also have used [idtac n] in place of [pose n], which would have printed the result without changing the context.
548 548
549 [n] only has the length calculation unrolled one step. What has happened here is that, by escaping into the [constr] nonterminal, we referred to the [length] function of Gallina, rather than the [length] Ltac function that we are defining. *) 549 [n] only has the length calculation unrolled one step. What has happened here is that, by escaping into the [constr] nonterminal, we referred to the [length] function of Gallina, rather than the [length] Ltac function that we are defining. *)
550 550
551 Abort. 551 Abort.
552 552