|
Module NamedContext.
Definition foo := true.
Section Foo.
Let bar := foo.
Eval native_compute in bar.
Eval vm_compute in bar.
End Foo.
End NamedContext.
Module RelContext.
Definition foo := true.
Definition bar (x := foo) := Eval native_compute in x.
Definition barvm (x := foo) := Eval vm_compute in x.
End RelContext.
¤ Dauer der Verarbeitung: 0.16 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.
|
