summaryrefslogtreecommitdiff
path: root/test-suite/output/Notations.out
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-08-06 16:15:08 -0400
committerGravatar Stephane Glondu <steph@glondu.net>2010-08-06 16:17:55 -0400
commitf18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (patch)
treec413c5bb42d20daf5307634ae6402526bb994fd6 /test-suite/output/Notations.out
parentb9f47391f7f259c24119d1de0a87839e2cc5e80c (diff)
Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg
Diffstat (limited to 'test-suite/output/Notations.out')
-rw-r--r--test-suite/output/Notations.out28
1 files changed, 28 insertions, 0 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 924030ba..215d9b68 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -46,6 +46,32 @@ fun x : nat => ifn x is succ n then n else 0
: bool
-4
: Z
+The command has indeed failed with message:
+=> Error: x should not be bound in a recursive pattern of the right-hand side.
+The command has indeed failed with message:
+=> Error: in the right-hand side, y and z should appear in
+ term position as part of a recursive pattern.
+The command has indeed failed with message:
+=> Error: The reference w was not found in the current environment.
+The command has indeed failed with message:
+=> Error: x is unbound in the right-hand side.
+The command has indeed failed with message:
+=> Error: in the right-hand side, y and z should appear in
+ term position as part of a recursive pattern.
+The command has indeed failed with message:
+=> Error: z is expected to occur in binding position in the right-hand side.
+The command has indeed failed with message:
+=> Error: as y is a non-closed binder, no such "," is allowed to occur.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Both ends of the recursive pattern are the same.
SUM (nat * nat) nat
: Set
FST (0; 1)
@@ -59,6 +85,8 @@ Defining 'I' as keyword
: Prop
[|1, 2, 3; 4, 5, 6|]
: Z * Z * Z * (Z * Z * Z)
+[|0 * (1, 2, 3); (4, 5, 6) * false|]
+ : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool))
fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
: (Z -> Z -> Z -> Z) -> Z
plus