Module a. LocalHint Extern 0 => progress subst. Goalforall T (x y : T) (P Q : _ -> Prop), x = y -> (P x -> Q x) -> P y -> Q y. Proof. intros. (* this should not fail *)
progress eauto. Defined. End a.
Module b. LocalHint Extern 0 => progress subst. Goalforall T (x y : T) (P Q : _ -> Prop), y = x -> (P x -> Q x) -> P y -> Q y. Proof. intros.
eauto. Defined. End b.
Module c. LocalHint Extern 0 => progress subst; eauto. Goalforall T (x y : T) (P Q : _ -> Prop), x = y -> (P x -> Q x) -> P y -> Q y. Proof. intros.
eauto. Defined. End c.
Module d. LocalHint Extern 0 => progress subst; repeatmatchgoalwith H : _ |- _ => revert H end. Goalforall T (x y : T) (P Q : _ -> Prop), x = y -> (P x -> Q x) -> P y -> Q y. Proof. intros.
debug eauto. Defined. End d.
(* An other variant which was still failing in 8.5 beta2 *)
Parameter A B : Prop. Axiom a:B.
#[export] Hint Extern 1 => matchgoalwith H:_ -> id _ |- _ => try (unfold id in H) end. Goal (B -> id A) -> A. intros.
eauto using a. Abort.
Messung V0.5 in Prozent
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.13Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 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.
