(* Use of idents bound to ltac names in a "match" *)
Definition foo : Type. Proof. let x := fresh "a" in
refine (forall k : nat * nat, let '(x, _) := k in (_ : Type)). exact (a = a). Defined. Goal foo. intros k. elim k. (* elim because elim keeps names *) intros. Check a. (* We check that the name is "a" *) 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.
