|
Set Nested Proofs Allowed.
Class Foo.
Class Bar := b : Type.
Set Refine Instance Mode.
Instance foo : Foo := _.
Unset Refine Instance Mode.
(* 1 subgoals, subgoal 1 (ID 4)
============================
Foo *)
Instance bar : Bar.
exact Type.
Defined.
(* bar is defined *)
About foo.
(* foo not a defined object. *)
Fail Defined.
¤ Dauer der Verarbeitung: 0.13 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.
|
