Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug_2310.v Sprache: Coq

Original von: Coq^©

(* Dependent higher-order hole in "refine" (simplified version) *)

Set Implicit Arguments.

Inductive Nest t := Cons : Nest (prod t t) -> Nest t.

Definition cast A x y Heq P H := @eq_rect A x P H y Heq.

Definition replace a (y:Nest (prod a a)) : a = a -> Nest a.

(* This used to raise an anomaly Unknown Meta in 8.2 and 8.3beta.
   It raises a regular error in 8.3 and almost succeeds with the new
   proof engine: there are two solutions to a unification problem
   (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either
   leave P as subgoal or choose itself one solution *)

  intros. Fail refine (Cons (cast H _ y)).
  Unset Solve Unification Constraints. (* Keep the unification constraint around *)
  refine (Cons (cast H _ y)).
  intros.
  refine (Nest (prod X X)). Qed.

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.