Quelle bug_2310.v Sprache: 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.

quality97%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.