| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/series/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 41 kB |
|
Quelle abstract_poly.v Sprache: Coq |
|||||||||
|
Set Universe Polymorphism.
Inductive path@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := refl : path x x. Inductive unit@{i} : Type@{i} := tt. Lemma foo@{i j} : forall (m n : unit@{i}) (P : unit -> Type@{j}), path m n -> P m -> P n. Proof. intros m n P e p. abstract (rewrite e in p; exact p). Defined. Check foo_subproof@{Set Set}. Lemma bar : forall (m n : unit) (P : unit -> Type), path m n -> P m -> P n. Proof. intros m n P e p. abstract (rewrite e in p; exact p). Defined. Check bar_subproof@{Set Set}. ¤ Dauer der Verarbeitung: 0.3 Sekunden ¤*© Formatika GbR, Deutschland |
|
2026-03-28