equal
deleted
inserted
replaced
10 |
10 |
11 subsection {* Basis for universal domain *} |
11 subsection {* Basis for universal domain *} |
12 |
12 |
13 subsubsection {* Basis datatype *} |
13 subsubsection {* Basis datatype *} |
14 |
14 |
15 types ubasis = nat |
15 type_synonym ubasis = nat |
16 |
16 |
17 definition |
17 definition |
18 node :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis set \<Rightarrow> ubasis" |
18 node :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis set \<Rightarrow> ubasis" |
19 where |
19 where |
20 "node i a S = Suc (prod_encode (i, prod_encode (a, set_encode S)))" |
20 "node i a S = Suc (prod_encode (i, prod_encode (a, set_encode S)))" |