Which proofs need a 'sorry'.
Smaller things:+ −
+ −
- case names for "weak" induction rules (names of the + −
constructors); see page 61/62 and 170 in Tutorial+ −
+ −
- <type>_perm rules should be added to the simplifier;+ −
maybe <type>_perm whould be called permute_<type>.simps;+ −
that would conform with the terminology in Nominal2+ −
+ −
- <type>_fv / <type>_bn / <type>_distinct should also be + −
added to the simplifier+ −
+ −
+ −
Bigger things:+ −
+ −
- nested recursion, like types "trm list" in a constructor+ −
+ −
- strong induction rules+ −
+ −
- show support equations+ −
+ −
- automate the proofs that are currently proved with sorry:+ −
alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp+ −