Quelle  Notations3.out   Sprache: unbekannt

{x : nat | x = 0} + {True /\ False} + {forall x : nat, x = 0}
     : Set
[<0, 2 >]
     : nat * nat * (nat * nat)
[<0, 2 >]
     : nat * nat * (nat * nat)
(0, 2, (2, 2))
     : nat * nat * (nat * nat)
pair (pair 0 2) (pair 2 0)
     : prod (prod nat nat) (prod nat nat)
<< 0, 2, 4 >>
     : nat * nat * nat * (nat * (nat * nat))
<< 0, 2, 4 >>
     : nat * nat * nat * (nat * (nat * nat))
(0, 2, 4, (2, (2, 0)))
     : nat * nat * nat * (nat * (nat * nat))
(0, 2, 4, (0, (2, 4)))
     : nat * nat * nat * (nat * (nat * nat))
pair (pair (pair 0 2) 4) (pair 4 (pair 2 0))
     : prod (prod (prod nat nat) nat) (prod nat (prod nat nat))
ETA x y : nat, Nat.add
     : nat -> nat -> nat
ETA x y : nat, Nat.add
     : nat -> nat -> nat
ETA x y : nat, Nat.add
     : nat -> nat -> nat
fun x y : nat => Nat.add x y
     : forall (_ : nat) (_ : nat), nat
ETA x y : nat, le_S
     : forall x y : nat, x <= y -> x <= S y
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]
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]
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]
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]
forall n : nat, {#n | 1 > n}
     : Prop
forall x : nat, {|x | x > 0|}
     : Prop
exists2 x : nat, x = 1 & x = 2
     : Prop
fun n : nat =>
foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + z = 0) z y x)
     : nat -> Prop
fun n : nat =>
foo2 n (fun a b c : nat => (fun _ _ _ : nat => a + b + c = 0) c b a)
     : nat -> Prop
fun n : nat =>
foo2 n (fun n0 y z : nat => (fun _ _ _ : nat => n0 + y + z = 0) z y n0)
     : nat -> Prop
fun n : nat =>
foo2 n (fun x n0 z : nat => (fun _ _ _ : nat => x + n0 + z = 0) z n0 x)
     : nat -> Prop
fun n : nat =>
foo2 n (fun x y n0 : nat => (fun _ _ _ : nat => x + y + n0 = 0) n0 y x)
     : nat -> Prop
fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2
     : nat -> Prop
fun n : nat => {|n, y | fun _ _ _ : nat => n + y = 0 |}_2
     : nat -> Prop
fun n : nat => {|n, n0 | fun _ _ _ : nat => n + n0 = 0 |}_2
     : nat -> Prop
fun n : nat =>
foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x)
     : nat -> Prop
fun n : nat =>
foo2 n (fun x y z : nat => (fun _ _ _ : nat => x + y + n = 0) z y x)
     : nat -> Prop
fun n : nat => {|n, fun _ : nat => 0 = 0 |}_3
     : nat -> Prop
fun n : nat => {|n, fun _ : nat => n = 0 |}_3
     : nat -> Prop
fun n : nat => foo3 n (fun x _ : nat => ETA z : nat, (fun _ : nat => x = 0))
     : nat -> Prop
fun n : nat => {|n, fun _ : nat => 0 = 0 |}_4
     : nat -> Prop
fun n : nat => {|n, fun _ : nat => n = 0 |}_4
     : nat -> Prop
fun n : nat => foo4 n (fun _ _ : nat => ETA z : nat, (fun _ : nat => z = 0))
     : nat -> Prop
fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0))
     : nat -> Prop
tele (t : Type) '(y, z) (x : t) := tt
     : forall t : Type, nat * nat -> t -> fpack
tele (t : Type) (y := nat) (x : t) (z : y) := (y, z)
     : forall t : Type, t -> nat -> 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))
File "./output/Notations3.v", line 179, characters 0-174:
Warning: Closed notations (i.e. starting and ending with a terminal symbol)
should usually be at level 0 (default).
[closed-notation-not-level-0,parsing,default]
letpair x [1] = {0};
return (1, 2, 3, 4)
     : nat * nat * nat * nat
((*1).2).3
     : nat
*(1.2)
     : nat
{{ 1 | 1 // 1 }}
     : nat
!!! _ _ : nat, True
     : (nat -> Prop) * ((nat -> Prop) * Prop)
! '{{x, y}}, x.y = 0
     : Prop
exists_mixed (x y : nat) '{{u, t}}, x.y = 0 /\ u.t = 0
     : Prop
exists_mixed (x y : nat) '{{z, t}}, 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
!! _ _ : nat # True #
     : Prop * Prop * Prop
{{D 1, 2}}
     : nat * nat * (nat * nat * (nat * nat))
! a b : nat # True #
     : Prop * (Prop * Prop)
{{forall x : nat, x = 0, nat}}
     : Prop * Set
!!!! 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 2 (pair 1 0)) (pair (pair 0 2) 1)) (pair 1 (pair 2 0)))
  (pair (pair 0 1) 2)
     : 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

Arguments foo l%_list_scope
Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
  : type_scope (default interpretation) (from Corelib.Init.Logic)
Notation "'exists' ! x .. y , p" :=
  (ex (unique (fun x => .. (ex (unique (fun y => p))) ..))) : type_scope
  (default interpretation) (from Corelib.Init.Logic)
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope
  (default interpretation) (from Corelib.Init.Datatypes)
1 goal
  
  ============================
  ##@%
   ^^^
myfoo01 tt
     : nat
myfoo01 tt
     : nat
myfoo01 tt
     : nat
1 ⪯ 2 ⪯ 3 ⪯ 4
     : Prop
1 goal
  
  x : nat
  ============================
  |-_0 x
1 goal
  
  xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx : nat
  ============================
  |-_0
   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx *
   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
FORALL [[a, b]], a - b = 0
     : Prop
∀ (A : TypTerm) (B : ◻ A -> TypTerm),
(∀ a : ◻ A, ◻ {B a}) -> ◻ (∀' {a : ◻ A}, {B a})
     : Type
FORALL [[a, b]], a - b = 0
     : Prop
∀ a b : nat, a - b = 0
     : Prop
fun x : option unit => match x with
                       | # tt & => # tt &
                       | None => None
                       end
     : option unit -> option unit