Function definitions+ −
+ −
- export proofs bout alpha_bn+ −
- equations like+ −
+ −
| "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)"+ −
+ −
do not work+ −
+ −
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+ −
+ −
- store information about defined nominal datatypes, so that+ −
it can be used to define new types that depend on these+ −
+ −