(* to be used e.g. in : coqtop -I src -R theories Tuto3 < theories/test.v *)
RequireImport 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.4 Sekunden
(vorverarbeitet)
¤
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.
