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+ −
+ −
+ −
What are the proofs that are still proved by sorry?+ −