|
(* A slight shortening of bug 6078 *)
(* This bug exposed a different behavior of unshelve_unifiable
depending on which projection is found in the unification
heuristics *)
Axiom flat_type : Type.
Axiom interp_flat_type : flat_type -> Type.
Inductive type := Arrow (_ _ : flat_type).
Definition interp_type (t : type)
:= interp_flat_type (match t with Arrow s d => s end)
-> interp_flat_type (match t with Arrow s d => d end).
Axiom Expr : type -> Type.
Axiom Interp : forall {t : type}, Expr t -> interp_type t.
Axiom Wf : forall {t}, Expr t -> Prop.
Axiom a : forall f, interp_flat_type f.
Definition packaged_expr_functionP A :=
(fun F : Expr A -> Expr A
=> forall e' v, Interp (F e') v = a (let (_,f) := A in f)).
Goal forall (f f0 : flat_type)
(e : forall _ : Expr (@Arrow f f0),
Expr (@Arrow f f0)),
@packaged_expr_functionP (@Arrow f f0) e.
intros.
refine (fun (e0 : Expr (Arrow f f0))
=> (fun zHwf':True =>
(fun v : interp_flat_type f =>
?[G] : ?[U] = ?[V] :> interp_flat_type ?[v])) ?[H]);
[ | ].
(* Was: Error: Tactic failure: Incorrect number of goals (expected 3 tactics). *)
Abort.
¤ Dauer der Verarbeitung: 0.31 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.
|
