X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fexamples%2Fautomath%2Fomega.aut;fp=helm%2Fsoftware%2Fhelena%2Fexamples%2Fautomath%2Fomega.aut;h=9e6c30e6f4ac681e2cc44c220797981685f6e919;hb=bbc1c6ccb596693c46f4d75d7875b94c79f1d575;hp=0000000000000000000000000000000000000000;hpb=30eb28f8c35d7667b3a0052c30d2750a492fa464;p=helm.git

diff --git a/helm/software/helena/examples/automath/omega.aut b/helm/software/helena/examples/automath/omega.aut
new file mode 100644
index 000000000..9e6c30e6f
--- /dev/null
+++ b/helm/software/helena/examples/automath/omega.aut
@@ -0,0 +1,8 @@
+# This book is not valid in AUT-QE because [y:'type'] is not allowed
+# This book is not valid in \lambda\delta < 3 because sort inclusion is not allowed
+# This book is not valid in \lambda\delta 3 because of two \upsilon-reductions on layer 1
+
++l
+@ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
+@ Omega := <Delta>Delta : 'type'
+-l