1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
(* to be used e.g. in : coqtop -I src -R theories Tuto3 < theories/test.v *)
Require Import Tuto3.Loader.
(* This should print Type. *)
Tuto3_1.
(* This should print a term that contains an existential variable. *)
(* And then print the same term, where the variable has been correctly
instantiated. *)
Tuto3_2.
Lemma tutu x y (A : 0 < x) (B : 10 < y) : True.
Proof.
pack hypothesis A.
(* Hypothesis A should have disappeared and a "packed_hyps" hypothesis
should have appeared, with unreadable content. *)
pack hypothesis B.
(* Hypothesis B should have disappeared *)
destruct packed_hyps as [unpacked_hyps].
(* Hypothesis unpacked_hyps should contain the previous contents of A and B. *)
exact I.
Qed.
|
