(** Alternative implementation of the hyp primitive *)
Ltac2 get_hyp_by_name x := let h := hyps () in let rec find x l := match l with
| [] => zero Not_found
| p :: l => match p with
| (id, _, t) => match Ident.equal x id with
| true => t
| false => find x l end end end in
find x h.
Print Ltac2 get_hyp_by_name.
Goalforall n m, n + m = 0 -> n = 0. Proof.
refine (fun () => '(fun n m H => _)). let t := get_hyp_by_name @H in Message.print (Message.of_constr t). 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.
