|
(* 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.
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
