(* A disjoint-names condition was missing when matching names in Ltac
pattern-matching *)
Goal True. let x := (eval cbv beta zeta in (fun P => let Q := P in fun P => P + Q)) in
unify x (fun a b => b + a); (* success *) let x' := lazymatch x with
| (fun (a : ?A) (b : ?B) => ?k)
=> constr:(fun (a : A) (b : B) => k) end in
unify x x'. Abort.
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.
