blob: a3f6ad9fa22cee97b4ae79d302ed51b20ab10816 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(* Outside a section, Hypothesis, Variable, Axiom all obey implicit binders *)
Hypothesis foo1 : forall {n : nat}, True.
Variable foo1' : forall {n : nat}, True.
Axiom foo1'' : forall {n : nat}, True.
Check foo1 (n := 1).
Check foo1' (n := 1).
Check foo1'' (n := 1).
Section bar.
(* Inside a section, Hypothesis and Variable do not, but they should *)
Hypothesis foo2 : forall {n : nat}, True.
Variable foo2' : forall {n : nat}, True.
Axiom foo2'' : forall {n : nat}, True.
Check foo2 (n := 1).
Check foo2' (n := 1).
Check foo2'' (n := 1).
End bar.
|
