regression tests

[helm.git] / helm / gTopLevel / tests / forall00.cic.test

diff --git a/helm/gTopLevel/tests/forall00.cic.test b/helm/gTopLevel/tests/forall00.cic.test
new file mode 100644 (file)
index 0000000..1665098
--- /dev/null
+++ b/helm/gTopLevel/tests/forall00.cic.test
@@ -0,0 +1,9 @@
+\forall n:nat. \forall m. n + m = n
+### (* METASENV after disambiguation  *)
+
+### (* TERM after disambiguation      *)
+(n:nat)(m:nat)(eq nat (plus n m) n)
+### (* TYPE_OF the disambiguated term *)
+Prop
+### (* REDUCED disambiguated term     *)
+(n:nat)(m:nat)(eq nat (plus n m) n)