Require Extraction.Set Universe Polymorphism.Definition foo@{s; |} := tt.Definition bar := foo@{Prop;}.(* the actual problem only appears once we have inductives with sort poly output: *) Inductive Pair@{s;u|} (A:Type @{s;u}) : Type @{s;u} := pair : A -> A -> Pair A.Definition use_pair@{s;+|} A (k:A->nat) (x:Pair@{s;_} A) :=match x with pair _ x _ => x end ).Definition make_pair := pair@{Prop;_} _ I I.Definition hell := use_pair True (fun _ => 0) make_pair.(* Some tests *) Module Foo.Definition foo@{s1 s2| |} := fun (A : Type @{s1|Set }) (x : A) => x.Definition foo0 := foo@{SProp Type |}.Definition foo1 := foo@{Type SProp|}.Inductive T@{s| |} : Type @{s|Set } := O : T | S : T -> T.Inductive box@{s1 s2| |} (A : Type @{s1|Set }) (B : Type @{s2|Set }) : Type @{Set } := Box : A -> B -> box A B.Definition bar (A : Type ) (x : A) := 0.Definition qux := bar (forall A : Prop, A -> A) foo@{Prop Type |}.End Foo.(* Check module subtyping *) Module Type S.Inductive box@{s1 s2| |} (A : Type @{s1|Set }) (B : Type @{s2|Set }) : Type @{Set } := Box : A -> B -> box A B.End S.Module Bar : S.Inductive box@{s1 s2| |} (A : Type @{s1|Set }) (B : Type @{s2|Set }) : Type @{Set } := Box : A -> B -> box A B.End Bar.quality 100%
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
