- Modularity
All files in the library have been converted to modules. lib_start_up imports parameters,
logic and Martin Löf equality. The default parameters
support ambiguity. This means that the command Make
should no longer be needed in modules. All dependencies should
now be declared via Import
- lib_list_basics
append_strict = ... : {t|SET}{k,l:list t}
(Eq (append k l) (nil t))->and (Eq k (nil t)) (Eq l (nil t))
- lib_ML
absurd_impl_empty = ... : absurd->empty
- lib_ML_nat
nat_diagonal = ... : {C|Type}(nat->C)->(nat->C)->nat->nat->C
nat_diagonal_const = ... : {C|Type}C->C->nat->nat->C
nat_filter = ... : nat->nat->Type
nat_Thm = ... : nat->nat->SET
nat_thm = ... : {u,v:nat}nat_Thm u v
with
fun nat_diagonal f _ a b = f a b if a and b stem from the same constructor
|nat_diagonal _ g a b = g a b
fun nat_diagonal_const f _ a b = f if a and b stem from the same constructor
|nat_diagonal_const g _ _ _ = g
val nat_filter = nat_diagonal_const unit empty
fun nat_Thm 0 0 = unit
|nat_Thm 0 (suc n) = {n:nat}(Eq 0 (suc n))->empty
|nat_Thm (suc m) 0 = {m:nat}(Eq (suc m) 0)->empty
|nat_Thm (suc m) (suc n) = injective suc
- lib_nat_Lt
Lt_resp_plus_right = ... : {a,x,y|nat}(Lt x y)->Lt x (plus a y)
complete_elimination = ... : {P:nat->TYPE}
({n:nat}({x:nat}(Lt x n)->P x)->P n)->
{m:nat}P m
well_founded_elimination = ... : {t|TYPE}{f:t->nat}{P:t->TYPE}
({x:t}({y:t}(Lt (f y) (f x))->P y)->P x)->
{z:t}P z
- Number theory
The modules have been revised to work for any
substitutive and symmetric equality.
- lib_Type
The directory lib_Type contains variants of other modules in which all occurrences of SET,
TYPE, TYPE_minus1 and TYPE_minus2 have been replaced by Type to support typical ambiguity.
