TODO
author Christian Urban <urbanc@in.tum.de>
Mon, 17 Jan 2011 12:33:37 +0000
changeset 2662 7c5bca978886
parent 2452 39f8d405d7a2
child 2719 dd5b60bccfd4
permissions -rw-r--r--
eliminated tracing code; added flag so that equivariance is only proved for the function graph, not the relation


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