equal
deleted
inserted
replaced
6 Codatatype definition of Lazy Lists |
6 Codatatype definition of Lazy Lists |
7 *) |
7 *) |
8 |
8 |
9 structure LList = CoDatatype_Fun |
9 structure LList = CoDatatype_Fun |
10 (val thy = QUniv.thy |
10 (val thy = QUniv.thy |
|
11 val thy_name = "LList" |
11 val rec_specs = [("llist", "quniv(A)", |
12 val rec_specs = [("llist", "quniv(A)", |
12 [(["LNil"], "i",NoSyn), |
13 [(["LNil"], "i",NoSyn), |
13 (["LCons"], "[i,i]=>i",NoSyn)])] |
14 (["LCons"], "[i,i]=>i",NoSyn)])] |
14 val rec_styp = "i=>i" |
15 val rec_styp = "i=>i" |
15 val sintrs = ["LNil : llist(A)", |
16 val sintrs = ["LNil : llist(A)", |