|
Set Primitive Projections.
(* This proof was accepted in Coq 8.5 because the subterm specs were not
projected correctly *)
Inductive foo : Prop := mkfoo { proj1 : False -> foo; proj2 : (forall P : Prop, P -> P) }.
Fail Fixpoint loop (x : foo) : False :=
loop (proj2 x _ x).
Fail Definition bad : False := loop (mkfoo (fun x => match x with end) (fun _ x => x)).
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
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.
|
