(* Testing a regression from 8.5beta1 to 8.5beta2 in evar-evar tactic unification problems *)
Inductive test : nat -> nat -> nat -> nat -> Prop :=
| test1 : forall m n, test m n m n.
Goal test 1234.
erewrite f_equal2 with (f := fun k l => test _ _ k l). Abort.
Messung V0.5 in Prozent
¤ 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.0.0Bemerkung:
(vorverarbeitet am 2026-06-04)
¤
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 und die Messung sind noch experimentell.
