equal
deleted
inserted
replaced
89 |
89 |
90 (* Sort constraints *) |
90 (* Sort constraints *) |
91 |
91 |
92 datatype ('a::finite, 'b::finite) F = F 'a | F2 'b |
92 datatype ('a::finite, 'b::finite) F = F 'a | F2 'b |
93 |
93 |
94 instance T :: (finite) finite by (default, transfer, auto) |
94 instance T :: (finite) finite by standard (transfer, auto) |
95 |
95 |
96 lift_definition(code_dt) f17 :: "bool \<Rightarrow> (bool T, 'b::finite) F" is "\<lambda>b. F b" by auto |
96 lift_definition(code_dt) f17 :: "bool \<Rightarrow> (bool T, 'b::finite) F" is "\<lambda>b. F b" by auto |
97 |
97 |
98 export_code f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 |
98 export_code f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 |
99 checking SML OCaml? Haskell? Scala? |
99 checking SML OCaml? Haskell? Scala? |