diff options
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 |