Ignore:
Timestamp:
Nov 29, 2010, 2:08:52 PM (10 years ago)
Author:
mulligan
Message:

Fixed segmentation fault in Nat.ma, added get_index and renamed previous get_index to get_index_weak in List.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/List.ma

    r329 r330  
    103103        #K;
    104104        ncases (K absd);
    105     ##| ncases (less_than_monoton);
    106    
    107    
     105    ##| nnormalize in p;
     106        nnormalize;
     107        napply (succ_less_than_or_equal_injective ? ?);
     108        nassumption;
     109    ##]
     110nqed.
     111       
    108112nlet rec get_index_weak (A: Type[0]) (l: List A) (n: Nat) on n ≝
    109113  match n with
     
    116120      match l with
    117121        [ Empty ⇒ Nothing A
    118         | Cons hd tl ⇒ get_index A tl o
     122        | Cons hd tl ⇒ get_index_weak A tl o
    119123        ]
    120124    ].
Note: See TracChangeset for help on using the changeset viewer.