|
Definition something (P:Type) (e:P) := e.
Inductive myunit : Set := mytt.
(* Proof below works when definition is in Type,
however builtin types such as unit are in Set. *)
Lemma demo_hide_generic :
let x := mytt in x = x.
Proof.
intros.
change mytt with (@something _ mytt) in x.
subst x. (* Proof works if this line is removed *)
reflexivity.
Qed.
¤ Dauer der Verarbeitung: 0.18 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.
|
