Changeset 1367 for src/common/AST.ma
 Timestamp:
 Oct 13, 2011, 5:48:09 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/AST.ma
r1353 r1367 199 199 200 200 lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2). 201 * *; try *; try *; try *; try *; try (%1 @refl) %2 @nmk #H cases daemon (*Wilmer: XXX*) qed. 201 * #H [#H2] * #H' (try #H2') try (%1 @refl) [2,3,4,6,7,8: %2 @nmk #abs destruct] 202 cases H cases H' try (%1 @refl) [1,5,9: cases H2 cases H2' try (%1 @refl)] 203 %2 @nmk #abs H H'; try (H2 H2') destruct (abs) (*Wilmer: still slow destructs, why?*) 204 qed. 202 205 203 206 lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
Note: See TracChangeset
for help on using the changeset viewer.