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
** Module lib_ML_nat Imports lib_empty lib_unit lib_nat nat_diagonal = ... : {C|Type}(nat->nat->C)->(nat->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