diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-08-06 16:15:08 -0400 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-08-06 16:17:55 -0400 |
| commit | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (patch) | |
| tree | c413c5bb42d20daf5307634ae6402526bb994fd6 /test-suite/output/Notations.out | |
| parent | b9f47391f7f259c24119d1de0a87839e2cc5e80c (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.out | 28 |
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 |