equal
deleted
inserted
replaced
3 |
3 |
4 Examples for coercive subtyping via subtype constraints. |
4 Examples for coercive subtyping via subtype constraints. |
5 *) |
5 *) |
6 |
6 |
7 theory Coercion_Examples |
7 theory Coercion_Examples |
8 imports Complex_Main |
8 imports Main |
9 begin |
9 begin |
|
10 |
|
11 declare[[coercion_enabled]] |
10 |
12 |
11 (* Error messages test *) |
13 (* Error messages test *) |
12 |
14 |
13 consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat" |
15 consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat" |
14 consts arg :: "int \<Rightarrow> nat" |
16 consts arg :: "int \<Rightarrow> nat" |