FIXME-TODO
changeset 527 9b1ad366827f
parent 525 3f657c4fbefa
child 529 6348c2a57ec2
equal deleted inserted replaced
526:7ba2fc25c6a3 527:9b1ad366827f
    10 
    10 
    11 - think about what happens if things go wrong (like
    11 - think about what happens if things go wrong (like
    12   theorem cannot be lifted) / proper diagnostic 
    12   theorem cannot be lifted) / proper diagnostic 
    13   messages for the user
    13   messages for the user
    14 
    14 
    15 - Ask Peter and Michael for challenging examples 
    15 - Ask Peter and Michael for challenging examples
       
    16   And for examples where it is useful to lift types
       
    17   over a relation being only a partial equivalence
    16 
    18 
    17 
    19 
    18 
    20 
    19 - Handle theorems that include Ball/Bex
    21 - Handle theorems that include Ball/Bex
    20 
    22