|
Require Import ProofIrrelevance.
Lemma proof_irrelevance_set : forall (P : Set) (p1 p2 : P), p1 = p2.
Fail exact proof_irrelevance.
(*Qed.
Lemma paradox : False.
assert (H : 0 <> 1) by discriminate.
apply H.
Fail apply proof_irrelevance. (* inlined version is rejected *)
apply proof_irrelevance_set.
Qed.*)
Abort.
¤ Dauer der Verarbeitung: 0.28 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.
|
