Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 536:d65e9c1c9041

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Touch-ups in 8.4
author Adam Chlipala <adam@chlipala.net>
date Wed, 05 Aug 2015 18:07:57 -0400
parents ed829eaa91b2
children 429e95d23b26
comparison
equal deleted inserted replaced
535:dac7a2705b00 536:d65e9c1c9041
1114 destruct ls; crush. 1114 destruct ls; crush.
1115 1115
1116 (** We can go further in automating the proof by exploiting the hint mechanism.%\index{Vernacular commands!Hint Extern}% *) 1116 (** We can go further in automating the proof by exploiting the hint mechanism.%\index{Vernacular commands!Hint Extern}% *)
1117 1117
1118 Restart. 1118 Restart.
1119 1119
1120 Hint Extern 1 (ntsize (match ?LS with Nil => _ | Cons _ _ => _ end) = _) => 1120 Hint Extern 1 (ntsize (match ?LS with Nil => _ | Cons _ _ => _ end) = _) =>
1121 destruct LS; crush. 1121 destruct LS; crush.
1122 induction tr1 using nat_tree_ind'; crush. 1122 induction tr1 using nat_tree_ind'; crush.
1123 Qed. 1123 Qed.
1124 (* end thide *) 1124 (* end thide *)