7 It has four contructors, of arities 0-3, and two parameters A and B. |
7 It has four contructors, of arities 0-3, and two parameters A and B. |
8 *) |
8 *) |
9 |
9 |
10 structure Data = Datatype_Fun |
10 structure Data = Datatype_Fun |
11 (val thy = Univ.thy |
11 (val thy = Univ.thy |
12 val thy_name = "Data" |
12 val thy_name = "Data" |
13 val rec_specs = [("data", "univ(A Un B)", |
13 val rec_specs = [("data", "univ(A Un B)", |
14 [(["Con0"], "i", NoSyn), |
14 [(["Con0"], "i", NoSyn), |
15 (["Con1"], "i=>i", NoSyn), |
15 (["Con1"], "i=>i", NoSyn), |
16 (["Con2"], "[i,i]=>i", NoSyn), |
16 (["Con2"], "[i,i]=>i", NoSyn), |
17 (["Con3"], "[i,i,i]=>i", NoSyn)])] |
17 (["Con3"], "[i,i,i]=>i", NoSyn)])] |