1 Function definitions

     2 

     3 - nominal_datatype should export proofs about alpha_bn: reflexivity, induction, ...?

     4 

     5 - nominal_datatype should declare xxx.fv_bn_eqvt as [eqvt]

     6 

     7 - equations that talk about True/False, for example

     8     | "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)"

     9   do not work (since 'function' does not work)

    10 

    11 - equivariance for functions can be derived automatically (knowing termination and

    12   equivariance of the graph).

    13 

    14 - for multiple simultanously defined functions, compatibility cases should fold the

    15   definition and derive eqvt_at for the folded one

    16 

    17 - equivariance of the graph for multiple functions does not use equivariance

    18   infrastructure

    19 

    20 Nominal_Datatype Parser should check that:

    21 

    22 - types of bindings match types of binding functions

    23 - fsets are not bound in lst bindings

    24 - bound arguments are not datatypes

    25 - binder is referred to by name and not by type

    26 

    27 Smaller things:

    28 

    29 - maybe <t1_t2>.perm_simps should be called permute_<type>.simps;

    30   that would conform with the terminology in Nominal2

    31 

    32 - nominal_induct does not work without an induction rule

    33 

    34 - nominal_induct throws strange "THM" exceptions if not enough

    35   variables are given

    36 

    37 - nominal_induct cannot avoid a term (for example function applied

    38   to an argument).

    39 

    40 - .induct and .exhaust could be the default methods for induction/cases

    41   on nominal datatypes

    42 

    43 Other:

    44 

    45 - nested recursion, like types "trm list" in a constructor

    46 

    47 - store information about defined nominal datatypes, so that

    48   it can be used to define new types that depend on these

    49