| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/bugs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 15.8.2025 mit Größe 807 B |
|
Quelle bug_3205.v Sprache: Coq |
|||||||||
|
Fail Fixpoint F (u : unit) : Prop :=
(fun p : {P : Prop & _} => match p with existT _ _ P => P end) (existT (fun P => False -> P) (F tt) _). (* Anomaly: A universe comparison can only happen between variables. Please report. *) Definition g (x : Prop) := x. Definition h (y : Type) := y. Definition eq_hf : h = g :> (Prop -> Type) := @eq_refl (Prop -> Type) g. Set Printing All. Set Printing Universes. Fail Definition eq_hf : h = g :> (Prop -> Type) := eq_refl g. (* Originally an anomaly, now says Toplevel input, characters 48-57: Error: The term "@eq_refl (forall _ : Prop, Prop) g" has type "@eq (forall _ : Prop, Prop) g g" while it is expected to have type "@eq (forall _ : Prop, Type (* Top.16 *) (Universe inconsistency: Cannot enforce Prop = Top.16)). *) ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28