Changeset 1600 for src/ASM/Util.ma


Ignore:
Timestamp:
Dec 13, 2011, 1:41:08 PM (8 years ago)
Author:
sacerdot
Message:

utilities and ASM ported to the new standard library

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1599 r1600  
    22include "basics/types.ma".
    33include "arithmetics/nat.ma".
    4 include "ASM/JMCoercions.ma".
     4include "basics/russell.ma".
    55
    66(* let's implement a daemon not used by automation *)
     
    271271  [ 1: normalize %
    272272  | 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 // ]
     275qed.
    279276   
    280277let rec map2_opt
Note: See TracChangeset for help on using the changeset viewer.