blob: d5409289c5c3bdb92e13e0ebabbc30a659d385f5 (
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
|
Require Import TestSuite.admit.
(* Test on definitions referring to section variables that are not any
longer in the current context *)
Section x.
Hypothesis h : forall(n : nat), n < S n.
Definition f(n m : nat)(less : n < m) : nat := n + m.
Lemma a : forall(n : nat), f n (S n) (h n) = 1 + 2 * n.
Proof.
(* XXX *) admit.
Qed.
Lemma b : forall(n : nat), n < 3 + n.
Proof.
clear.
intros n.
Fail assert (H := a n).
Abort.
Let T := True.
Definition p := I : T.
Lemma paradox : False.
Proof.
clear.
set (T := False).
Fail pose proof p as H.
Abort.
|
