Ltac2: Take some small APIs from rewriter (fst/snd)

coq · Jan 22, 2024 · 24067ea · 24067ea
1 parent 3298e47
commit 24067ea
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v
@@ -41,6 +41,11 @@ Ltac2 Type ('a, 'b, 'c, 'd) format.
 Ltac2 Type exn := [ .. ].
 Ltac2 Type 'a array.
 
+(** Tuples *)
+
+Ltac2 fst (p:'a * 'b) : 'a := let (x,_) := p in x.
+Ltac2 snd (p:'a * 'b) : 'b := let (_,y) := p in y.
+
 (** Pervasive types *)
 
 Ltac2 Type 'a option := [ None | Some ('a) ].