Changeset 1075 for src/ASM/Util.ma


Ignore:
Timestamp:
Jul 18, 2011, 5:21:14 PM (8 years ago)
Author:
mulligan
Message:

nearly completed rtl -> ertl pass removing all option types with dep. types

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1071 r1075  
    152152
    153153let rec split
    154   (A: Type[0]) (l: list A) (index: nat) (proof: index < |l|)
     154  (A: Type[0]) (l: list A) (index: nat) (proof: index |l|)
    155155    on index ≝
    156   match index return λx. x < |l| → (list A) × (list A) with
     156  match index return λx. x |l| → (list A) × (list A) with
    157157  [ O ⇒ λzero_prf. 〈[], l〉
    158158  | S index' ⇒ λsucc_prf.
    159     match l return λx. S index' < |x| → (list A) × (list A) with
     159    match l return λx. S index' |x| → (list A) × (list A) with
    160160    [ nil ⇒ λnil_absrd. ?
    161161    | cons hd tl ⇒ λcons_prf.
     
    165165  ] proof.
    166166  [1: normalize in nil_absrd;
    167       cases(not_le_Sn_O (S index'))
     167      cases(not_le_Sn_O index')
    168168      #HYP
    169169      cases(HYP nil_absrd)
    170170  |2: normalize in cons_prf;
    171       normalize
    172171      @le_S_S_to_le
    173172      assumption
Note: See TracChangeset for help on using the changeset viewer.