| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/modules/ (NIST Cobol Test-Suite ©) Datei vom 15.8.2025 mit Größe 1 kB |
|
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.
¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-09-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-10-10