equal
deleted
inserted
replaced
|
1 theory Codec_Class |
|
2 imports Common "Classy.Classy" |
|
3 begin |
|
4 |
|
5 ML.class codec = \<open>'a codec\<close> |
|
6 |
|
7 ML.instance \<open>Codec.unit\<close> :: codec |
|
8 ML.instance \<open>Codec.bool\<close> :: codec |
|
9 ML.instance \<open>Codec.string\<close> :: codec |
|
10 ML.instance \<open>Codec.int\<close> :: codec |
|
11 ML.instance \<open>Codec.list\<close> :: codec |
|
12 ML.instance \<open>Codec.tuple\<close> :: codec |
|
13 ML.instance \<open>Codec.option\<close> :: codec |
|
14 ML.instance \<open>Codec.either\<close> :: codec |
|
15 ML.instance \<open>Codec.triple\<close> :: codec |
|
16 ML.instance \<open>Codec.sort\<close> :: codec |
|
17 ML.instance \<open>Codec.typ\<close> :: codec |
|
18 ML.instance \<open>Codec.term\<close> :: codec |
|
19 ML.instance \<open>Codec.tree\<close> :: codec |
|
20 |
|
21 end |