src/HOLCF/Tools/holcf_library.ML
changeset 40212 20df78048db5
parent 40024 a0f760ef6995
child 40217 656bb85f01ab
equal deleted inserted replaced
40099:0fb7891f0c7c 40212:20df78048db5
   172 
   172 
   173 (*** Lifted unit type ***)
   173 (*** Lifted unit type ***)
   174 
   174 
   175 val oneT = @{typ "one"};
   175 val oneT = @{typ "one"};
   176 
   176 
   177 fun one_when_const T = Const (@{const_name one_when}, T ->> oneT ->> T);
   177 fun one_case_const T = Const (@{const_name one_case}, T ->> oneT ->> T);
   178 fun mk_one_when t = one_when_const (fastype_of t) ` t;
   178 fun mk_one_case t = one_case_const (fastype_of t) ` t;
   179 
   179 
   180 
   180 
   181 (*** Strict product type ***)
   181 (*** Strict product type ***)
   182 
   182 
   183 fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);
   183 fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);