blob: 023791050f7cb5bdbb8298e6e636287e0e372a99 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
Require Import Ltac2.Ltac2.
Import Ltac2.Control.
(** 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.
Goal forall 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.
|
