equal
deleted
inserted
replaced
1 Function definitions |
1 Function definitions |
2 |
2 |
3 - export proofs bout alpha_bn |
3 - export proofs bout alpha_bn |
|
4 - equations like |
4 |
5 |
|
6 | "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)" |
|
7 |
|
8 do not work |
5 |
9 |
6 Parser should check that: |
10 Parser should check that: |
7 |
11 |
8 - types of bindings match types of binding functions |
12 - types of bindings match types of binding functions |
9 - fsets are not bound in lst bindings |
13 - fsets are not bound in lst bindings |