Mercurial > cpdt > repo

comparison src/Tactics.v @ 64:739c2818d6e2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Co-inductive evaluation example
author Adam Chlipala <adamc@hcoop.net>
date Tue, 30 Sep 2008 17:47:59 -0400
parents 1a664ff9d2d1
children 21bb59c56b98
comparison
equal deleted inserted replaced
63:fe7d37dfbd26 64:739c2818d6e2
101 end 101 end
102 end 102 end
103 end. 103 end.
104 104
105 Ltac crush' lemmas invOne := 105 Ltac crush' lemmas invOne :=
106 let sintuition := simpl in *; intuition; repeat (simplHyp invOne; intuition); try congruence 106 let sintuition := simpl in *; intuition; subst; repeat (simplHyp invOne; intuition; subst); try congruence
107 in (sintuition; rewriter; 107 in (sintuition; rewriter;
108 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); 108 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
109 repeat (simplHyp invOne; intuition)); 109 repeat (simplHyp invOne; intuition));
110 sintuition; try omega). 110 sintuition; try omega).
111 111