| changeset 3841 | 22bbc1676768 |
| parent 3840 | e0baea4d485a |
| child 11316 | b4e71bd751e4 |
| 3840:e0baea4d485a | 3841:22bbc1676768 |
|---|---|
14 inductive |
14 inductive |
15 domains "listn(A)" <= "nat*list(A)" |
15 domains "listn(A)" <= "nat*list(A)" |
16 intrs |
16 intrs |
17 NilI "<0,Nil> : listn(A)" |
17 NilI "<0,Nil> : listn(A)" |
18 ConsI "[| a: A; <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)" |
18 ConsI "[| a: A; <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)" |
19 type_intrs "nat_typechecks @ list. intrs" |
19 type_intrs "nat_typechecks @ list.intrs" |
20 end |
20 end |