|
(* Checking that the "in" clause takes the "eqn" clause into account *)
Definition test (x: nat): {y: nat | False }. Admitted.
Parameter x: nat.
Parameter z: nat.
Goal
proj1_sig (test x) = z ->
False.
Proof.
intro H.
destruct (test x) eqn:Heqs in H.
change (test x = exist (fun _ : nat => False) x0 f) in Heqs. (* Check it has the expected statement *)
Abort.
¤ Dauer der Verarbeitung: 0.14 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.
|
