equal
deleted
inserted
replaced
22 |
22 |
23 - nested recursion, like types "trm list" in a constructor |
23 - nested recursion, like types "trm list" in a constructor |
24 |
24 |
25 - strong induction rules |
25 - strong induction rules |
26 |
26 |
27 - show support equations |
27 - check support equations for more bindings per constructor |
28 |
28 |
29 - automate the proofs that are currently proved with sorry: |
29 - automate the proofs that are currently proved with sorry: |
30 alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp |
30 alpha_equivp, fv_rsp, alpha_bn_rsp |
31 |
31 |
32 - store information about defined nominal datatypes, so that |
32 - store information about defined nominal datatypes, so that |
33 it can be used to define new types that depend on these |
33 it can be used to define new types that depend on these |
34 |
34 |
35 - make 3 versions of Abs |
35 - make 3 versions of Abs |