diff options
-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 |