ind_syntax.ML
changeset 134 4b7da5a895e7
parent 128 89669c58e506
child 182 d5c6d1fb236b
equal deleted inserted replaced
133:4a2bb4fbc168 134:4b7da5a895e7
    57 
    57 
    58 (** Cartesian product type **)
    58 (** Cartesian product type **)
    59 
    59 
    60 fun mk_prod (T1,T2) = Type("*", [T1,T2]);
    60 fun mk_prod (T1,T2) = Type("*", [T1,T2]);
    61 
    61 
    62 fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
    62 (*Maps the type T1*...*Tn to [T1,...,Tn], if nested to the right*)
       
    63 fun factors (Type("*", [T1,T2])) = T1 :: factors T2
    63   | factors T                    = [T];
    64   | factors T                    = [T];
    64 
    65 
    65 (*Make a correctly typed ordered pair*)
    66 (*Make a correctly typed ordered pair*)
    66 fun mk_Pair (t1,t2) = 
    67 fun mk_Pair (t1,t2) = 
    67   let val T1 = fastype_of t1
    68   let val T1 = fastype_of t1