|
(* 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.14 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.
|
