Quelle export_inst.v Sprache: Coq

Class Foo.

Module Foo.

#[export]
Instance F : Foo := {}.

End Foo.

Fail Definition foo_test := let _ : Foo := _ in tt.

Import Foo.

Definition foo_test := let _ : Foo := _ in tt.

Class Bar.

Module Bar.

Section Bar.

Variable b : Bar.

#[export] Instance B : Bar := {}.

(* Cannot declare variables as export instances *)
Fail #[export] Existing Instance b.

End Bar.

Definition bar_test := let _ : Bar := _ in tt.

End Bar.

Fail Definition bar_test := let _ : Bar := _ in tt.

Import Bar.

Definition bar_test := let _ : Bar := _ in tt.

quality100%

¤ Dauer der Verarbeitung: 0.2 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.