equal
deleted
inserted
replaced
8 We use list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z) |
8 We use list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z) |
9 and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z) |
9 and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z) |
10 so that list can serve as a "functor" for defining other recursive types |
10 so that list can serve as a "functor" for defining other recursive types |
11 *) |
11 *) |
12 |
12 |
13 SList = Sexp + |
13 SList = Sexp + Hilbert_Choice (*gives us "inv"*) + |
14 |
14 |
15 consts |
15 consts |
16 |
16 |
17 list :: 'a item set => 'a item set |
17 list :: 'a item set => 'a item set |
18 NIL :: 'a item |
18 NIL :: 'a item |