blob: 7bfb2fc21083ed51dadaab9c517289e3c7e4982c (
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
|
Nat.sub : nat -> nat -> nat
Nat.sub is not universe polymorphic
Arguments Nat.sub _%nat_scope _%nat_scope : simpl nomatch
Nat.sub is transparent
Expands to: Constant Coq.Init.Nat.sub
Nat.sub : nat -> nat -> nat
Nat.sub is not universe polymorphic
Arguments Nat.sub _%nat_scope / _%nat_scope : simpl nomatch
Nat.sub is transparent
Expands to: Constant Coq.Init.Nat.sub
Nat.sub : nat -> nat -> nat
Nat.sub is not universe polymorphic
Arguments Nat.sub !_%nat_scope / _%nat_scope : simpl nomatch
Nat.sub is transparent
Expands to: Constant Coq.Init.Nat.sub
Nat.sub : nat -> nat -> nat
Nat.sub is not universe polymorphic
Arguments Nat.sub !_%nat_scope !_%nat_scope /
Nat.sub is transparent
Expands to: Constant Coq.Init.Nat.sub
Nat.sub : nat -> nat -> nat
Nat.sub is not universe polymorphic
Arguments Nat.sub !_%nat_scope !_%nat_scope
Nat.sub is transparent
Expands to: Constant Coq.Init.Nat.sub
pf :
forall D1 C1 : Type,
(D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
pf is not universe polymorphic
Arguments pf {D1%foo_scope} {C1%type_scope} _ [D2] [C2] : simpl never
pf is transparent
Expands to: Constant Arguments.pf
fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
fcomp is not universe polymorphic
Arguments fcomp {A%type_scope} {B%type_scope} {C%type_scope} _ _ _ /
fcomp is transparent
Expands to: Constant Arguments.fcomp
volatile : nat -> nat
volatile is not universe polymorphic
Arguments volatile / _%nat_scope
volatile is transparent
Expands to: Constant Arguments.volatile
f : T1 -> T2 -> nat -> unit -> nat -> nat
f is not universe polymorphic
Arguments f _ _ _%nat_scope _ _%nat_scope
f is transparent
Expands to: Constant Arguments.S1.S2.f
f : T1 -> T2 -> nat -> unit -> nat -> nat
f is not universe polymorphic
Arguments f _ _ !_%nat_scope !_ !_%nat_scope
f is transparent
Expands to: Constant Arguments.S1.S2.f
f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
f is not universe polymorphic
Arguments f [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope
f is transparent
Expands to: Constant Arguments.S1.f
f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
f is not universe polymorphic
Arguments f [T1%type_scope] [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope
f is transparent
Expands to: Constant Arguments.f
= forall v : unit, f 0 0 5 v 3 = 2
: Prop
= 2 = 2
: Prop
f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
f is not universe polymorphic
Arguments f _ _ _ _ !_ !_ !_
f is transparent
Expands to: Constant Arguments.f
forall w : r, w 3 true = tt
: Prop
The command has indeed failed with message:
Unknown interpretation for notation "$".
w 3 true = tt
: Prop
The command has indeed failed with message:
Extra arguments: _, _.
volatilematch : nat -> nat
volatilematch is not universe polymorphic
Arguments volatilematch / _%nat_scope : simpl nomatch
volatilematch is transparent
Expands to: Constant Arguments.volatilematch
= fun n : nat => volatilematch n
: nat -> nat
|
