wf_types.why 299 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11
theory Test
    type t 'a

    type test 'a = Test (t (test 'a))
end

theory Main
    type id 'a = 'a
    type shell 'a = Shell 'a
    type option 'a = Some 'a | None

12
(*
13 14
    clone Test as T1 with type t = id
    clone Test as T2 with type t = shell
15
*)
16 17
    clone Test as T3 with type t = option
end