Function definitions+
−
+
−
- export proofs bout alpha_bn+
−
+
−
+
−
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+
−
+
−