(* 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. Inductivetype := 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)). Goalforall (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.14 Sekunden
(vorverarbeitet)
¤
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.
