TODO
changeset 1580 0faec4f7d737
parent 1576 7b8f570b2450
child 1649 ba837d3ed37f
equal deleted inserted replaced
1579:5b0bdd64956e 1580:0faec4f7d737
    25 - strong induction rules
    25 - strong induction rules
    26 
    26 
    27 - check support equations for more bindings per constructor
    27 - check support equations for more bindings per constructor
    28 
    28 
    29 - automate the proofs that are currently proved with sorry:
    29 - automate the proofs that are currently proved with sorry:
    30   alpha_equivp, alpha_bn_rsp
    30   alpha_equivp
    31 
    31 
    32 - store information about defined nominal datatypes, so that
    32 - store information about defined nominal datatypes, so that
    33   it can be used to define new types that depend on these
    33   it can be used to define new types that depend on these
    34 
    34 
    35 - make parser aware of bn functions that call other bn functions
    35 - make parser aware of bn functions that call other bn functions