equal
deleted
inserted
replaced
19 |
19 |
20 - show support equations |
20 - show support equations |
21 |
21 |
22 - automate the proofs that are currently proved with sorry: |
22 - automate the proofs that are currently proved with sorry: |
23 alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp |
23 alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp |
|
24 |
|
25 - store information about defined nominal datatypes, so that |
|
26 it can be used to define new types that depend on these |
|
27 |
|
28 - make 3 versions of Abs |
|
29 |
|
30 - make parser aware of recursive and of different versions of abs |