Changeset 1600 for src/ASM/Util.ma
- Timestamp:
- Dec 13, 2011, 1:41:08 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Util.ma
r1599 r1600 2 2 include "basics/types.ma". 3 3 include "arithmetics/nat.ma". 4 include " ASM/JMCoercions.ma".4 include "basics/russell.ma". 5 5 6 6 (* let's implement a daemon not used by automation *) … … 271 271 [ 1: normalize % 272 272 | 2: normalize % 273 | 3: normalize 274 generalize in match (sig2 … (reduce_strong A B tl tl1)); 275 >p2 >p3 >p4 normalize in ⊢ (% → ?); 276 #HYP // 277 ] 278 qed. 273 | 3: normalize >p3 in p2; >p4 cases (reduce_strong … tl tl1) normalize 274 #X #H #EQ destruct // ] 275 qed. 279 276 280 277 let rec map2_opt
Note: See TracChangeset
for help on using the changeset viewer.