functor-datatype-test.timl

functor FunctorDatatypeTest1Fn (FunctorDatatypeTest1Fn_K : sig
                                  (* type ttt = int *)
               datatype ttt 'a : {Nat} =
                        Nil of ttt 'a {0}
                      | Cons {n_sig : Nat} of 'a * ttt 'a {n_sig} --> ttt 'a {n_sig + 1}
              end) = struct
end
        
structure FunctorDatatypeTest1Arg = struct
(* type ttt = int *)
datatype ttt 'a : {Nat} =
         Nil of ttt 'a {0}
       | Cons {n_impl : Nat} of 'a * ttt 'a {n_impl} --> ttt 'a {n_impl + 1}
end

structure FunctorDatatypeTest1Result = FunctorDatatypeTest1Fn (FunctorDatatypeTest1Arg)

functor FunctorDatatypeTest2Fn (FunctorDatatypeTest2Fn_T : sig
  type table 'a  {Nat} {Nat}
  (* type ttt = table *)
  datatype do_delete 'a {num size : Nat} = DoDelete {num' : Nat} {num = num' \/ num = num' + 1} of table 'a {size} {num'} --> do_delete 'a {size} {num}
end) = struct
end

structure FunctorDatatypeTest2Arg = struct
  datatype table 'a {size : Nat} {num : Nat} = DummyTable of table 'a {0} {0}
  (* type ttt = table *)
  datatype do_delete 'a {num size : Nat} = DoDelete {num' : Nat} {num = num' \/ num = num' + 1} of table 'a {size} {num'} --> do_delete 'a {size} {num}
end

structure FunctorDatatypeTest2Result = FunctorDatatypeTest2Fn (FunctorDatatypeTest2Arg)