aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Notations3.out
blob: ffea0819a50a5ba0a9d9f0f381915314260c737c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
[<0, 2 >]
     : nat * nat * (nat * nat)
[<0, 2 >]
     : nat * nat * (nat * nat)
(0, 2, (2, 2))
     : nat * nat * (nat * nat)
pair (pair O (S (S O))) (pair (S (S O)) O)
     : 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 O (S (S O))) (S (S (S (S O)))))
  (pair (S (S (S (S O)))) (pair (S (S O)) O))
     : 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 : 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)