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
|
minus : nat -> nat -> nat
Argument scopes are [nat_scope nat_scope]
The simpl tactic unfolds minus avoiding to expose match constructs
minus is transparent
Expands to: Constant Coq.Init.Peano.minus
minus : nat -> nat -> nat
Argument scopes are [nat_scope nat_scope]
The simpl tactic unfolds minus when applied to 1 argument
avoiding to expose match constructs
minus is transparent
Expands to: Constant Coq.Init.Peano.minus
minus : nat -> nat -> nat
Argument scopes are [nat_scope nat_scope]
The simpl tactic unfolds minus
when the 1st argument evaluates to a constructor and
when applied to 1 argument avoiding to expose match constructs
minus is transparent
Expands to: Constant Coq.Init.Peano.minus
minus : nat -> nat -> nat
Argument scopes are [nat_scope nat_scope]
The simpl tactic unfolds minus
when the 1st and 2nd arguments evaluate to a constructor and
when applied to 2 arguments
minus is transparent
Expands to: Constant Coq.Init.Peano.minus
minus : nat -> nat -> nat
Argument scopes are [nat_scope nat_scope]
The simpl tactic unfolds minus
when the 1st and 2nd arguments evaluate to a constructor
minus is transparent
Expands to: Constant Coq.Init.Peano.minus
pf :
forall D1 C1 : Type,
(D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
Arguments D2, C2 are implicit
Arguments D1, C1 are implicit and maximally inserted
Argument scopes are [foo_scope type_scope _ _ _ _ _]
The simpl tactic never unfolds pf
pf is transparent
Expands to: Constant Top.pf
fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
Arguments A, B, C are implicit and maximally inserted
Argument scopes are [type_scope type_scope type_scope _ _ _]
The simpl tactic unfolds fcomp when applied to 6 arguments
fcomp is transparent
Expands to: Constant Top.fcomp
volatile : nat -> nat
Argument scope is [nat_scope]
The simpl tactic always unfolds volatile
volatile is transparent
Expands to: Constant Top.volatile
f : T1 -> T2 -> nat -> unit -> nat -> nat
Argument scopes are [_ _ nat_scope _ nat_scope]
f is transparent
Expands to: Constant Top.S1.S2.f
f : T1 -> T2 -> nat -> unit -> nat -> nat
Argument scopes are [_ _ nat_scope _ nat_scope]
The simpl tactic unfolds f
when the 3rd, 4th and 5th arguments evaluate to a constructor
f is transparent
Expands to: Constant Top.S1.S2.f
f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
Argument T2 is implicit
Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
The simpl tactic unfolds f
when the 4th, 5th and 6th arguments evaluate to a constructor
f is transparent
Expands to: Constant Top.S1.f
f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
Arguments T1, T2 are implicit
Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
The simpl tactic unfolds f
when the 5th, 6th and 7th arguments evaluate to a constructor
f is transparent
Expands to: Constant Top.f
f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
The simpl tactic unfolds f
when the 5th, 6th and 7th arguments evaluate to a constructor
f is transparent
Expands to: Constant Top.f
forall w : r, w 3 true = tt
: Prop
The command has indeed failed with message:
=> Error: Unknown interpretation for notation "$".
w 3 true = tt
: Prop
The command has indeed failed with message:
=> Error: Extra argument _.
|
