diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-08 08:57:37 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-08 08:57:37 +0000 |
| commit | b21fc973b24e944eb412efdc924d31119d412328 (patch) | |
| tree | caaa13c39c1bfca62e85ca40fe4745afda900fde /etc/lego | |
| parent | 835a23242167d7f59a47f9f5295368b91e47daa6 (diff) | |
Error example from Randy, showing too much info was lost in output msgs.
Diffstat (limited to 'etc/lego')
| -rw-r--r-- | etc/lego/error-eg.l | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/etc/lego/error-eg.l b/etc/lego/error-eg.l new file mode 100644 index 00000000..f6872c90 --- /dev/null +++ b/etc/lego/error-eg.l @@ -0,0 +1,16 @@ +Init LF; + +[prop:Type]; +[prf:prop->Type]; +[type:Type]; +[el:type->Type]; + +[FA : {A:type}((el A) -> prop) -> prop]; +[LL : {A:type}{P:(el A) -> prop} + ({x:el A}prf(P(x)))-> + (********************************) + prf(FA A P)]; + +[P_FA : {A:type}{P:(el A) -> prop}{C_FA:prf(FA A P) -> prop} + ((g:{x:el A}prf(P(x)))prf(C_FA(LL A P g))) -> + {z:prf(FA A P)}prf(C_FA(z))];
\ No newline at end of file |