TODO
changeset 2876 99583bd6a7b2
parent 2874 1628e47fa57c
equal deleted inserted replaced
2875:ab2aded5f7c9 2876:99583bd6a7b2
    35   variables are given
    35   variables are given
    36 
    36 
    37 - nominal_induct cannot avoid a term (for example function applied
    37 - nominal_induct cannot avoid a term (for example function applied
    38   to an argument).
    38   to an argument).
    39 
    39 
       
    40 - .induct and .exhaust could be the default methods for induction/cases
       
    41   on nominal datatypes
       
    42 
    40 Other:
    43 Other:
    41 
    44 
    42 - nested recursion, like types "trm list" in a constructor
    45 - nested recursion, like types "trm list" in a constructor
    43 
    46 
    44 - store information about defined nominal datatypes, so that
    47 - store information about defined nominal datatypes, so that