aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Cases.out
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/Cases.out')
-rw-r--r--test-suite/output/Cases.out13
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 95fcd362e..8ce6f9795 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -59,3 +59,16 @@ end
The command has indeed failed with message:
Non exhaustive pattern-matching: no clause found for pattern
gadtTy _ _
+The command has indeed failed with message:
+In environment
+texpDenote : forall t : type, texp t -> typeDenote t
+t : type
+e : texp t
+t1 : type
+t2 : type
+t0 : type
+b : tbinop t1 t2 t0
+e1 : texp t1
+e2 : texp t2
+The term "0" has type "nat" while it is expected to have type
+ "typeDenote t0".