diff options
Diffstat (limited to 'test-suite/output/Notations.out')
| -rw-r--r-- | test-suite/output/Notations.out | 30 |
1 files changed, 23 insertions, 7 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 215d9b68..66307236 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -2,10 +2,10 @@ true ? 0; 1 : nat if true as x return (x ? nat; bool) then 0 else true : nat -Defining 'proj1' as keyword +Identifier 'proj1' now a keyword fun e : nat * nat => proj1 e : nat * nat -> nat -Defining 'decomp' as keyword +Identifier 'decomp' now a keyword decomp (true, true) as t, u in (t, u) : bool * bool !(0 = 0) @@ -28,18 +28,18 @@ forall n n0 : nat, ###(n = n0) : list nat (1; 2, 4) : nat * nat * nat -Defining 'ifzero' as keyword +Identifier 'ifzero' now a keyword ifzero 3 : bool -Defining 'pred' as keyword +Identifier 'pred' now a keyword pred 3 : nat fun n : nat => pred n : nat -> nat fun n : nat => pred n : nat -> nat -Defining 'ifn' as keyword -Defining 'is' as keyword +Identifier 'ifn' now a keyword +Identifier 'is' now a keyword fun x : nat => ifn x is succ n then n else 0 : nat -> nat 1- @@ -80,7 +80,7 @@ Nil : forall A : Type, list A NIL:list nat : list nat -Defining 'I' as keyword +Identifier 'I' now a keyword (false && I 3)%bool /\ I 6 : Prop [|1, 2, 3; 4, 5, 6|] @@ -120,3 +120,19 @@ fun x : option Z => match x with | NONE3 => 0 end : option Z -> Z +s + : s +Identifier 'foo' now a keyword +10 + : nat +fun _ : nat => 9 + : nat -> nat +Identifier 'ONE' now a keyword +fun (x : nat) (p : x = x) => match p with + | ONE => ONE + end = p + : forall x : nat, x = x -> Prop +fun (x : nat) (p : x = x) => match p with + | 1 => 1 + end = p + : forall x : nat, x = x -> Prop |