diff options
Diffstat (limited to 'test-suite/output/Notations3.out')
| -rw-r--r-- | test-suite/output/Notations3.out | 156 |
1 files changed, 152 insertions, 4 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 360f3796..5ab61616 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -1,3 +1,5 @@ +{x : nat | x = 0} + {True /\ False} + {forall x : nat, x = 0} + : Set [<0, 2 >] : nat * nat * (nat * nat) [<0, 2 >] @@ -31,24 +33,24 @@ fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f : (forall x : nat * (bool * unit), ?T) -> forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))} where -?T : [x : nat * (bool * unit) |- Type] +?T : [x : nat * (bool * unit) |- Type] fun f : forall x : bool * (nat * unit), ?T => CURRYINV (x : nat) (y : bool), f : (forall x : bool * (nat * unit), ?T) -> forall (x : nat) (y : bool), ?T@{x:=(y, (x, tt))} where -?T : [x : bool * (nat * unit) |- Type] +?T : [x : bool * (nat * unit) |- Type] fun f : forall x : unit * nat * bool, ?T => CURRYLEFT (x : nat) (y : bool), f : (forall x : unit * nat * bool, ?T) -> forall (x : nat) (y : bool), ?T@{x:=(tt, x, y)} where -?T : [x : unit * nat * bool |- Type] +?T : [x : unit * nat * bool |- Type] fun f : forall x : unit * bool * nat, ?T => CURRYINVLEFT (x : nat) (y : bool), f : (forall x : unit * bool * nat, ?T) -> forall (x : nat) (y : bool), ?T@{x:=(tt, y, x)} where -?T : [x : unit * bool * nat |- Type] +?T : [x : unit * bool * nat |- Type] forall n : nat, {#n | 1 > n} : Prop forall x : nat, {|x | x > 0|} @@ -98,3 +100,149 @@ fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0)) : nat -> Prop tele (t : Type) '(y, z) (x : t0) := tt : forall t : Type, nat * nat -> t -> fpack +[fun x : nat => x + 0;; fun x : nat => x + 1;; fun x : nat => x + 2] + : (nat -> nat) * + ((nat -> nat) * + ((nat -> nat) * + ((nat -> nat) * ((nat -> nat) * ((nat -> nat) * (nat -> nat)))))) +foo5 x nat x + : nat -> nat +fun x : ?A => x === x + : forall x : ?A, x = x +where +?A : [x : ?A |- Type] (x cannot be used) +{{0, 1}} + : nat * nat +{{0, 1, 2}} + : nat * (nat * nat) +{{0, 1, 2, 3}} + : nat * (nat * (nat * nat)) +letpair x [1] = {0}; +return (1, 2, 3, 4) + : nat * nat * nat * nat +{{ 1 | 1 // 1 }} + : nat +!!! _ _ : nat, True + : (nat -> Prop) * ((nat -> Prop) * Prop) +((*1).2).3 + : nat +*(1.2) + : nat +! '{{x, y}}, x.y = 0 + : Prop +exists x : nat, + nat -> + exists y : nat, + nat -> exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x.y = 0 /\ u.t = 0 + : Prop +exists x : nat, + nat -> + exists y : nat, + nat -> exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x.y = 0 /\ z.t = 0 + : Prop +exists_true '{{x, y}} (u := 0) '{{z, t}}, x.y = 0 /\ z.t = 0 + : Prop +exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R), +(forall x : A, R x x) + : Prop +exists_true (x : nat) (A : Type) (R : A -> A -> Prop) +(_ : Reflexive R) (y : nat), x.y = 0 -> forall z : A, R z z + : Prop +{{{{True, nat -> True}}, nat -> True}} + : Prop * Prop * Prop +{{D 1, 2}} + : nat * nat * (nat * nat * (nat * nat)) +! a b : nat # True # + : Prop * (Prop * Prop) +!!!! a b : nat # True # + : Prop * Prop * (Prop * Prop * Prop) +@@ a b : nat # a = b # b = a # + : Prop * Prop +exists_non_null x y z t : nat , x = y /\ z = t + : Prop +forall_non_null x y z t : nat , x = y /\ z = t + : Prop +{{RL 1, 2}} + : nat * (nat * nat) +{{RR 1, 2}} + : nat * nat * nat +@pair nat (prod nat nat) (S (S O)) (@pair nat nat (S O) O) + : prod nat (prod nat nat) +@pair (prod nat nat) nat (@pair nat nat O (S (S O))) (S O) + : prod (prod nat nat) nat +{{RLRR 1, 2}} + : nat * (nat * nat) * (nat * nat * nat) * (nat * (nat * nat)) * + (nat * nat * nat) +pair + (pair + (pair (pair (S (S O)) (pair (S O) O)) (pair (pair O (S (S O))) (S O))) + (pair (S O) (pair (S (S O)) O))) (pair (pair O (S O)) (S (S O))) + : prod + (prod (prod (prod nat (prod nat nat)) (prod (prod nat nat) nat)) + (prod nat (prod nat nat))) (prod (prod nat nat) nat) +fun x : nat => if x is n .+ 1 then n else 1 + : nat -> nat +{'{{x, y}} : nat * nat | x.y = 0} + : Set +exists2' {{x, y}}, x = 0 & y = 0 + : Prop +myexists2 x : nat * nat, + let '{{y, z}} := x in y > z & let '{{y, z}} := x in z > y + : Prop +fun '({{x, y}} as z) => x.y = 0 /\ z = z + : nat * nat -> Prop +myexists ({{x, y}} as z), x.y = 0 /\ z = z + : Prop +exists '({{x, y}} as z), x.y = 0 /\ z = z + : Prop +∀ '({{x, y}} as z), x.y = 0 /\ z = z + : Prop +fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x.y + : nat * nat * bool -> nat +myexists ({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y + : Prop +exists '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y + : Prop +∀ '({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y + : Prop +fun p : nat => if p is S n then n else 0 + : nat -> nat +fun p : comparison => if p is Lt then 1 else 0 + : comparison -> nat +fun S : nat => [S | S.S] + : nat -> nat * (nat -> nat) +fun N : nat => [N | N.0] + : nat -> nat * (nat -> nat) +fun S : nat => [[S | S.S]] + : nat -> nat * (nat -> nat) +{I : nat | I = I} + : Set +{'I : True | I = I} + : Prop +{'{{x, y}} : nat * nat | x.y = 0} + : Set +exists2 '{{y, z}} : nat * nat, y > z & z > y + : Prop +foo = +fun l : list nat => match l with + | _ :: (_ :: _) as l1 => l1 + | _ => l + end + : list nat -> list nat + +Argument scope is [list_scope] +Notation +"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope +(default interpretation) +"'exists' ! x .. y , p" := ex + (unique + (fun x => .. (ex (unique (fun y => p))) ..)) +: type_scope (default interpretation) +Notation +"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope +(default interpretation) +1 subgoal + + ============================ + ##@% + ^^^ |