Definition foo0 (p : Foo) := match p with {| |} => tt end. Definition foo1 (p : Foo) := match p with {| foo := f |} => f end. Definition foo2 (p : Foo) := match p with {| foo := f; |} => f end. Definition foo3 (p : Foo) := match p with {| foo := f; bar := g |} => (f, g) end. Definition foo4 (p : Foo) := match p with {| foo := f; bar := g; |} => (f, g) end.
End A.
Module B.
Record Foo := { }.
End B.
Module C.
Record Foo := { foo : unit; bar : unit; }.
Definition foo_ := {|
foo := tt;
bar := tt;
|}.
End C.
Module D.
Record Foo := { foo : unit }. Definition foo_ := {| foo := tt |}.
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.
