|
Section foo.
Context (x := 1).
Definition foo : x = 1 := eq_refl.
End foo.
Module Type Foo.
Context (x := 1).
Definition foo : x = 1 := eq_refl.
End Foo.
Set Universe Polymorphism.
Inductive unit := tt.
Inductive eq {A} (x y : A) : Type := eq_refl : eq x y.
Section bar.
Context (x := tt).
Definition bar : eq x tt := eq_refl _ _.
End bar.
Module Type Bar.
Context (x := tt).
Definition bar : eq x tt := eq_refl _ _.
End Bar.
¤ Dauer der Verarbeitung: 0.12 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.
|
