TODO
changeset 1576 7b8f570b2450
parent 1573 b39108f42638
child 1649 ba837d3ed37f
equal deleted inserted replaced
1575:2c37f5a8c747 1576:7b8f570b2450
    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