equal
deleted
inserted
replaced
15 [(["Fnil"], "i"), |
15 [(["Fnil"], "i"), |
16 (["Fcons"], "[i,i]=>i")])]; |
16 (["Fcons"], "[i,i]=>i")])]; |
17 val rec_styp = "i=>i"; |
17 val rec_styp = "i=>i"; |
18 val ext = None |
18 val ext = None |
19 val sintrs = |
19 val sintrs = |
20 ["[| a:A; tf: forest(A) |] ==> Tcons(a,tf) : tree(A)", |
20 ["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)", |
21 "Fnil : forest(A)", |
21 "Fnil : forest(A)", |
22 "[| t: tree(A); tf: forest(A) |] ==> Fcons(t,tf) : forest(A)"]; |
22 "[| t: tree(A); f: forest(A) |] ==> Fcons(t,f) : forest(A)"]; |
23 val monos = []; |
23 val monos = []; |
24 val type_intrs = datatype_intrs |
24 val type_intrs = datatype_intrs |
25 val type_elims = datatype_elims); |
25 val type_elims = datatype_elims); |
26 |
26 |
27 val [TconsI, FnilI, FconsI] = TF.intrs; |
27 val [TconsI, FnilI, FconsI] = TF.intrs; |