Ignore:
Timestamp:
Nov 15, 2010, 10:28:26 AM (9 years ago)
Author:
mulligan
Message:

Got List to compile.

File:
1 edited

Legend:

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

    r241 r242  
    55include "Util.ma".
    66
    7 include "Universes/Universes.ma".
    8 
    9 include "Datatypes/Nat/Nat.ma".
    10 include "Datatypes/Nat/Addition.ma".
    11 
    12 include "Datatypes/Maybe.ma".
     7include "logic/pts.ma".
     8
     9include "Nat.ma".
     10
     11include "Maybe.ma".
    1312
    1413include "Plogic/equality.ma".
     
    167166  λl: List A.
    168167    remove_all_with_aux A f a l (Empty A).
    169    
    170 ncheck remove_all_with.
    171168
    172169nlet rec drop_while (A: Type[0]) (f: A → Bool) (l: List A) on l ≝
Note: See TracChangeset for help on using the changeset viewer.