Quelle coercions_nonuniform.v Sprache: Coq

(* Test the nonuniform attribute to silence warnings on coercions
not satisfying the non uniform inheritance condition. *)

Module Test0.

Parameter C : nat -> bool -> Type.
Parameter D : Type.
Parameter f : forall (n : nat) (b : bool), C n b -> D.

(* uniform inheritance satisfied, no warning *)
Coercion f : C >-> D.

End Test0.

Module Test1.

Parameter C : nat -> bool -> Type.
Parameter D : Type.
Parameter f : forall (b : bool) (n : nat), C n b -> D.

(* uniform inheritance not satisfied, warning *)
Coercion f : C >-> D.

End Test1.

Module Test2.

Parameter C : nat -> bool -> Type.
Parameter D : Type.
Parameter f : forall (b : bool) (n : nat), C n b -> D.

(* uniform inheritance not satisfied but attribute, no warning *)
#[warning="-uniform-inheritance"] Coercion f : C >-> D.

End Test2.

Module Test3.

Parameter C : nat -> bool -> Type.
Parameter D : Type.
Parameter f : forall (n : nat) (b : bool), C n b -> D.

(* uniform inheritance satisfied, no warning *)
Coercion f' := f.

End Test3.

Module Test4.

Parameter C : nat -> bool -> Type.
Parameter D : Type.
Parameter f : forall (b : bool) (n : nat), C n b -> D.

(* uniform inheritance not satisfied, warning *)
Coercion f' := f.

End Test4.

Module Test5.

Parameter C : nat -> bool -> Type.
Parameter D : Type.
Parameter f : forall (b : bool) (n : nat), C n b -> D.

(* uniform inheritance not satisfied but attribute, no warning *)
#[warning="-uniform-inheritance"] Coercion f' := f.

End Test5.

quality97%

¤ Dauer der Verarbeitung: 0.4 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.