the TypeError exception is back in place inside the Type modules

[helm.git] / helm / software / lambda-delta / automath / Omega.aut

diff --git a/helm/software/lambda-delta/automath/Omega.aut b/helm/software/lambda-delta/automath/Omega.aut
new file mode 100644 (file)
index 0000000..661154d
--- /dev/null
+++ b/helm/software/lambda-delta/automath/Omega.aut
@@ -0,0 +1,10 @@
+# The lambda-term \Omega
+# This book is not accepted in AUT-QE because [y:'type'] is not allowed
+# This book is accepted in lambda-delta with sort inclusion but Omega is not
+#    valid if sort inclusion is allowed on the term backbone only
+# This book is valid in lambda-delta with sort inclusion allowed everywhere 
+
++l 
+@ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
+  Omega := <Delta>Delta             : 'type'
+-l