Quelle subtyping.v Sprache: Coq

(* Non regression for bug #1302 *)

(* With universe polymorphism for inductive types, subtyping of
   inductive types needs a special treatment: the standard conversion
   algorithm does not work as it only knows to deal with constraints of
   the form alpha = beta or max(alphas, alphas+1) <= beta, while
   subtyping of inductive types in Type generates constraints of the form
   max(alphas, alphas+1) <= max(betas, betas+1).

   These constraints are anyway valid by monotonicity of subtyping but we
   have to detect it early enough to avoid breaking the standard
   algorithm for constraints on algebraic universes. *)

Module Type T.

Parameter A : Type (* Top.1 *) .

Inductive L : Type (* max(Top.1,1) *) :=
| L0
| L1 :  (A -> Prop) -> L.

End T.

Axiom Tp : Type (* Top.5 *) .

Module TT : T.

Definition A : Type (* Top.6 *) := Tp. (* generates Top.5 <= Top.6 *)

Inductive L : Type (* max(Top.6,1) *) :=
| L0
| L1 :  (A -> Prop) -> L.

End TT. (* Generates Top.6 <= Top.1 (+ auxiliary constraints for L_rect) *)

(* Note: Top.6 <= Top.1 is generated by subtyping on A;
   subtyping of L follows and has not to be checked *)

(* The same bug as #1302 but for Definition *)
(* Check that inferred algebraic universes in interfaces are considered *)

Module Type U. Definition A := Type -> Type. End U.
Module M:U. Definition A := Type -> Type. End M.

quality100%

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

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.