equal
deleted
inserted
replaced
9 imports Semilat |
9 imports Semilat |
10 begin |
10 begin |
11 |
11 |
12 datatype 'a err = Err | OK 'a |
12 datatype 'a err = Err | OK 'a |
13 |
13 |
14 types 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err" |
14 type_synonym 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err" |
15 'a esl = "'a set * 'a ord * 'a ebinop" |
15 type_synonym 'a esl = "'a set * 'a ord * 'a ebinop" |
16 |
16 |
17 primrec ok_val :: "'a err \<Rightarrow> 'a" where |
17 primrec ok_val :: "'a err \<Rightarrow> 'a" where |
18 "ok_val (OK x) = x" |
18 "ok_val (OK x) = x" |
19 |
19 |
20 definition lift :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)" where |
20 definition lift :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)" where |