+ −
Parser should check that:+ −
+ −
- types of bindings match types of binding functions+ −
- fsets are not bound in lst bindings+ −
- bound arguments are not datatypes+ −
- binder is referred to by name and not by type+ −
+ −
Smaller things:+ −
+ −
- maybe <type>_perm whould be called permute_<type>.simps;+ −
that would conform with the terminology in Nominal2+ −
+ −
+ −
Other:+ −
+ −
- nested recursion, like types "trm list" in a constructor+ −
+ −
- define permute_bn automatically and prove properties of it+ −
+ −
- prove renaming-of-binders lemmas+ −
+ −
- strong induction rules+ −
+ −
- store information about defined nominal datatypes, so that+ −
it can be used to define new types that depend on these+ −
+ −