aboutsummaryrefslogtreecommitdiff
path: root/user-contrib
diff options
context:
space:
mode:
Diffstat (limited to 'user-contrib')
-rw-r--r--user-contrib/Ltac2/Bool.v63
-rw-r--r--user-contrib/Ltac2/Init.v3
-rw-r--r--user-contrib/Ltac2/Int.v15
-rw-r--r--user-contrib/Ltac2/List.v606
-rw-r--r--user-contrib/Ltac2/Option.v27
5 files changed, 714 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/Bool.v b/user-contrib/Ltac2/Bool.v
new file mode 100644
index 0000000000..413746acbd
--- /dev/null
+++ b/user-contrib/Ltac2/Bool.v
@@ -0,0 +1,63 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+
+Ltac2 andb x y :=
+ match x with
+ | true => y
+ | false => false
+ end.
+
+Ltac2 orb x y :=
+ match x with
+ | true => true
+ | false => y
+ end.
+
+Ltac2 implb x y :=
+ match x with
+ | true => y
+ | false => true
+ end.
+
+Ltac2 negb x :=
+ match x with
+ | true => false
+ | false => true
+ end.
+
+Ltac2 xorb x y :=
+ match x with
+ | true
+ => match y with
+ | true => false
+ | false => true
+ end
+ | false
+ => match y with
+ | true => true
+ | false => false
+ end
+ end.
+
+Ltac2 eqb x y :=
+ match x with
+ | true
+ => match y with
+ | true => true
+ | false => false
+ end
+ | false
+ => match y with
+ | true => false
+ | false => true
+ end
+ end.
diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v
index dc1690bdfb..c47aa82b05 100644
--- a/user-contrib/Ltac2/Init.v
+++ b/user-contrib/Ltac2/Init.v
@@ -66,5 +66,8 @@ Ltac2 Type exn ::= [ Not_found ].
Ltac2 Type exn ::= [ Match_failure ].
(** Used to signal a pattern didn't match a term. *)
+Ltac2 Type exn ::= [ Invalid_argument (message option) ].
+(** Used to signal that an invalid argument was passed to a tactic. *)
+
Ltac2 Type exn ::= [ Tactic_failure (message option) ].
(** Generic error for tactic failure. *)
diff --git a/user-contrib/Ltac2/Int.v b/user-contrib/Ltac2/Int.v
index 0a90d757b6..d88f8a70f3 100644
--- a/user-contrib/Ltac2/Int.v
+++ b/user-contrib/Ltac2/Int.v
@@ -16,3 +16,18 @@ Ltac2 @ external add : int -> int -> int := "ltac2" "int_add".
Ltac2 @ external sub : int -> int -> int := "ltac2" "int_sub".
Ltac2 @ external mul : int -> int -> int := "ltac2" "int_mul".
Ltac2 @ external neg : int -> int := "ltac2" "int_neg".
+
+Ltac2 lt (x : int) (y : int) := equal (compare x y) -1.
+Ltac2 gt (x : int) (y : int) := equal (compare x y) 1.
+Ltac2 le (x : int) (y : int) :=
+ (* we might use [lt x (add y 1)], but that has the wrong behavior on MAX_INT *)
+ match equal x y with
+ | true => true
+ | false => lt x y
+ end.
+Ltac2 ge (x : int) (y : int) :=
+ (* we might use [lt (add x 1) y], but that has the wrong behavior on MAX_INT *)
+ match equal x y with
+ | true => true
+ | false => gt x y
+ end.
diff --git a/user-contrib/Ltac2/List.v b/user-contrib/Ltac2/List.v
new file mode 100644
index 0000000000..10bef5a9bf
--- /dev/null
+++ b/user-contrib/Ltac2/List.v
@@ -0,0 +1,606 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+Require Ltac2.Int.
+Require Ltac2.Control.
+Require Ltac2.Bool.
+Require Ltac2.Message.
+
+Ltac2 rec length (ls : 'a list) :=
+ match ls with
+ | [] => 0
+ | _ :: xs => Int.add 1 (length xs)
+ end.
+
+Ltac2 rec compare_lengths (ls1 : 'a list) (ls2 : 'b list) :=
+ match ls1 with
+ | []
+ => match ls2 with
+ | [] => 0
+ | _ :: _ => -1
+ end
+ | _ :: ls1
+ => match ls2 with
+ | [] => 1
+ | _ :: ls2 => compare_lengths ls1 ls2
+ end
+ end.
+
+Ltac2 rec compare_length_with (ls : 'a list) (n : int) :=
+ match Int.lt n 0 with
+ | true => 1
+ | false
+ => match ls with
+ | [] => Int.compare 0 n
+ | _ :: ls => compare_length_with ls (Int.sub n 1)
+ end
+ end.
+
+Ltac2 cons (x : 'a) (xs : 'a list) :=
+ x :: xs.
+
+Ltac2 hd_opt (ls : 'a list) :=
+ match ls with
+ | [] => None
+ | x :: xs => Some x
+ end.
+
+Ltac2 hd_default (default : 'a) (ls : 'a list) :=
+ match hd_opt ls with
+ | Some v => v
+ | None => default
+ end.
+
+Ltac2 hd (ls : 'a list) :=
+ match ls with
+ | [] => Control.zero (Tactic_failure (Some (Message.of_string "hd")))
+ | x :: xs => x
+ end.
+
+Ltac2 tl (ls : 'a list) :=
+ match ls with
+ | [] => []
+ | x :: xs => xs
+ end.
+
+Ltac2 rec last_opt (ls : 'a list) :=
+ match ls with
+ | [] => None
+ | x :: xs
+ => match xs with
+ | [] => Some x
+ | _ :: _ => last_opt xs
+ end
+ end.
+
+Ltac2 last_default (default : 'a) (ls : 'a list) :=
+ match last_opt ls with
+ | None => default
+ | Some v => v
+ end.
+
+Ltac2 last (ls : 'a list) :=
+ match last_opt ls with
+ | None => Control.zero (Tactic_failure (Some (Message.of_string "last")))
+ | Some v => v
+ end.
+
+Ltac2 rec removelast (ls : 'a list) :=
+ match ls with
+ | [] => []
+ | x :: xs
+ => match xs with
+ | [] => []
+ | _ :: _ => x :: removelast xs
+ end
+ end.
+
+Ltac2 rec nth_opt_aux (ls : 'a list) (n : int) :=
+ match ls with
+ | [] => None
+ | x :: xs
+ => match Int.equal n 0 with
+ | true => Some x
+ | false => nth_opt_aux xs (Int.sub n 1)
+ end
+ end.
+
+Ltac2 nth_opt (ls : 'a list) (n : int) :=
+ match Int.lt n 0 with
+ | true => Control.zero (Invalid_argument (Some (Message.of_string "List.nth")))
+ | false => nth_opt_aux ls n
+ end.
+
+Ltac2 nth_default (default : 'a) (ls : 'a list) (n : int) :=
+ match nth_opt ls n with
+ | Some v => v
+ | None => default
+ end.
+
+Ltac2 nth (ls : 'a list) (n : int) :=
+ match nth_opt ls n with
+ | Some v => v
+ | None => Control.zero Out_of_bounds
+ end.
+
+Ltac2 rec rev_append (l1 : 'a list) (l2 : 'a list) :=
+ match l1 with
+ | [] => l2
+ | a :: l => rev_append l (a :: l2)
+ end.
+
+Ltac2 rev l := rev_append l [].
+
+Ltac2 rec append ls1 ls2 :=
+ match ls1 with
+ | [] => ls2
+ | x :: xs => x :: append xs ls2
+ end.
+
+Ltac2 app ls1 ls2 := append ls1 ls2.
+
+Ltac2 rec concat (ls : 'a list list) :=
+ match ls with
+ | [] => []
+ | x :: xs => app x (concat xs)
+ end.
+Ltac2 flatten (ls : 'a list list) := concat ls.
+
+Ltac2 rec iter (f : 'a -> unit) (ls : 'a list) :=
+ match ls with
+ | [] => ()
+ | l :: ls => f l; iter f ls
+ end.
+
+Ltac2 rec iteri_aux (i : int) (f : int -> 'a -> unit) (ls : 'a list) :=
+ match ls with
+ | [] => ()
+ | l :: ls => f i l; iteri_aux (Int.add i 1) f ls
+ end.
+
+Ltac2 iteri (f : int -> 'a -> unit) (ls : 'a list) :=
+ iteri_aux 0 f ls.
+
+Ltac2 rec map (f : 'a -> 'b) (ls : 'a list) :=
+ match ls with
+ | [] => []
+ | l :: ls => f l :: map f ls
+ end.
+
+Ltac2 rec mapi_aux (i : int) (f : int -> 'a -> 'b) (ls : 'a list) :=
+ match ls with
+ | [] => []
+ | l :: ls => f i l :: mapi_aux (Int.add i 1) f ls
+ end.
+
+Ltac2 mapi (f : int -> 'a -> 'b) (ls : 'a list) :=
+ mapi_aux 0 f ls.
+
+Ltac2 rec flat_map (f : 'a -> 'b list) (xs : 'a list) :=
+ match xs with
+ | [] => []
+ | x :: xs => append (f x) (flat_map f xs)
+ end.
+
+(* from the OCaml std lib *)
+Ltac2 rev_map (f : 'a -> 'b) (ls : 'a list) :=
+ let rec rmap_f accu ls :=
+ match ls with
+ | [] => accu
+ | a::l => rmap_f (f a :: accu) l
+ end in
+ rmap_f [] ls.
+
+Ltac2 rec fold_right (f : 'a -> 'b -> 'b) (a : 'b) (ls : 'a list) :=
+ match ls with
+ | [] => a
+ | l :: ls => f l (fold_right f a ls)
+ end.
+
+Ltac2 rec fold_left (f : 'a -> 'b -> 'a) (xs : 'b list) (a : 'a) :=
+ match xs with
+ | [] => a
+ | x :: xs => fold_left f xs (f a x)
+ end.
+
+Ltac2 rec iter2 (f : 'a -> 'b -> unit) (ls1 : 'a list) (ls2 : 'b list) :=
+ match ls1 with
+ | []
+ => match ls2 with
+ | [] => ()
+ | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.iter2")))
+ end
+ | l1 :: ls1
+ => match ls2 with
+ | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.iter2")))
+ | l2 :: ls2
+ => f l1 l2; iter2 f ls1 ls2
+ end
+ end.
+
+Ltac2 rec map2 (f : 'a -> 'b -> 'c) (ls1 : 'a list) (ls2 : 'b list) :=
+ match ls1 with
+ | []
+ => match ls2 with
+ | [] => []
+ | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.map2")))
+ end
+ | l1 :: ls1
+ => match ls2 with
+ | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.map2")))
+ | l2 :: ls2
+ => f l1 l2 :: map2 f ls1 ls2
+ end
+ end.
+
+(* from the OCaml std lib *)
+Ltac2 rev_map2 (f : 'a -> 'b -> 'c) (ls1 : 'a list) (ls2 : 'b list) :=
+ let rec rmap2_f accu ls1 ls2 :=
+ match ls1 with
+ | []
+ => match ls2 with
+ | [] => accu
+ | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.rev_map2")))
+ end
+ | l1 :: ls1
+ => match ls2 with
+ | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.rev_map2")))
+ | l2 :: ls2
+ => rmap2_f (f l1 l2 :: accu) ls1 ls2
+ end
+ end in
+ rmap2_f [] ls1 ls2.
+
+Ltac2 rec fold_right2 (f : 'a -> 'b -> 'c -> 'c) (a : 'c) (ls1 : 'a list) (ls2 : 'b list) :=
+ match ls1 with
+ | []
+ => match ls2 with
+ | [] => a
+ | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.fold_right2")))
+ end
+ | l1 :: ls1
+ => match ls2 with
+ | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.fold_right2")))
+ | l2 :: ls2
+ => f l1 l2 (fold_right2 f a ls1 ls2)
+ end
+ end.
+
+Ltac2 rec fold_left2 (f : 'a -> 'b -> 'c -> 'a) (ls1 : 'b list) (ls2 : 'c list) (a : 'a) :=
+ match ls1 with
+ | []
+ => match ls2 with
+ | [] => a
+ | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.fold_left2")))
+ end
+ | l1 :: ls1
+ => match ls2 with
+ | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.fold_left2")))
+ | l2 :: ls2
+ => fold_left2 f ls1 ls2 (f a l1 l2)
+ end
+ end.
+
+Ltac2 rec for_all f ls :=
+ match ls with
+ | [] => true
+ | x :: xs => match f x with
+ | true => for_all f xs
+ | false => false
+ end
+ end.
+
+(* we would call this [exists] a la OCaml's [List.exists], but that's a syntax error, so instead we name it after Coq's [existsb] *)
+Ltac2 rec existsb f ls :=
+ match ls with
+ | [] => false
+ | x :: xs => match f x with
+ | true => true
+ | false => existsb f xs
+ end
+ end.
+Ltac2 forallb f ls := for_all f ls.
+
+Ltac2 rec for_all2_aux f f_x f_y xs ys :=
+ match xs with
+ | [] => for_all f_y ys
+ | x :: xs'
+ => match ys with
+ | [] => for_all f_x xs
+ | y :: ys'
+ => match f x y with
+ | true => for_all2_aux f f_x f_y xs' ys'
+ | false => false
+ end
+ end
+ end.
+Ltac2 for_all2 f xs ys :=
+ let on_different_lengths () :=
+ Control.zero (Invalid_argument (Some (Message.of_string "List.for_all2"))) in
+ for_all2_aux
+ f (fun _ => on_different_lengths ()) (fun _ => on_different_lengths ())
+ xs ys.
+Ltac2 forallb2 f xs ys := for_all2 f xs ys.
+Ltac2 rec exists2_aux f f_x f_y xs ys :=
+ match xs with
+ | [] => existsb f_y ys
+ | x :: xs'
+ => match ys with
+ | [] => existsb f_x xs
+ | y :: ys'
+ => match f x y with
+ | true => true
+ | false => exists2_aux f f_x f_y xs' ys'
+ end
+ end
+ end.
+Ltac2 existsb2 f xs ys :=
+ let on_different_lengths () :=
+ Control.zero (Invalid_argument (Some (Message.of_string "List.existsb2"))) in
+ exists2_aux
+ f (fun _ => on_different_lengths ()) (fun _ => on_different_lengths ())
+ xs ys.
+
+Ltac2 rec find_opt f xs :=
+ match xs with
+ | [] => None
+ | x :: xs => match f x with
+ | true => Some x
+ | false => find_opt f xs
+ end
+ end.
+Ltac2 rec find f xs :=
+ match find_opt f xs with
+ | Some v => v
+ | None => Control.zero Not_found
+ end.
+Ltac2 rec find_rev_opt f xs :=
+ match xs with
+ | [] => None
+ | x :: xs => match find_rev_opt f xs with
+ | Some v => Some v
+ | None => match f x with
+ | true => Some x
+ | false => None
+ end
+ end
+ end.
+Ltac2 find_rev f xs :=
+ match find_rev_opt f xs with
+ | Some v => v
+ | None => Control.zero Not_found
+ end.
+
+Ltac2 mem (eq : 'a -> 'a -> bool) (a : 'a) (ls : 'a list) :=
+ match find_opt (eq a) ls with
+ | Some _ => true
+ | None => false
+ end.
+
+Ltac2 rec filter f xs :=
+ match xs with
+ | [] => []
+ | x :: xs
+ => match f x with
+ | true => x :: filter f xs
+ | false => filter f xs
+ end
+ end.
+Ltac2 rec filter_out f xs :=
+ filter (fun x => Bool.negb (f x)) xs.
+
+Ltac2 find_all (f : 'a -> bool) (ls : 'a list) := filter f ls.
+
+Ltac2 remove (eqb : 'a -> 'a -> bool) (x : 'a) (ls : 'a list) :=
+ filter_out (eqb x) ls.
+
+Ltac2 count_occ (eqb : 'a -> 'a -> bool) (x : 'a) (ls : 'a list) :=
+ length (filter (eqb x) ls).
+
+(* from the Coq stdlib *)
+Ltac2 rec list_power (ls1 : 'a list) (ls2 : 'b list) :=
+ match ls1 with
+ | [] => [] :: []
+ | x :: t
+ => flat_map (fun f => map (fun y => (x, y) :: f) ls2)
+ (list_power t ls2)
+ end.
+
+Ltac2 rec partition (f : 'a -> bool) (l : 'a list) :=
+ match l with
+ | [] => ([], [])
+ | x :: tl
+ => let (g, d) := partition f tl in
+ match f x with
+ | true => ((x::g), d)
+ | false => (g, (x::d))
+ end
+ end.
+
+(* from the Coq stdlib *)
+(** [list_prod] has the same signature as [combine], but unlike
+ [combine], it adds every possible pairs, not only those at the
+ same position. *)
+
+Ltac2 rec list_prod (ls1 : 'a list) (ls2 : 'b list) :=
+ match ls1 with
+ | [] => []
+ | x :: t
+ => app (map (fun y => (x, y)) ls2) (list_prod t ls2)
+ end.
+
+Ltac2 rec firstn (n : int) (ls : 'a list) :=
+ match Int.lt n 0 with
+ | true => Control.zero (Invalid_argument (Some (Message.of_string "List.firstn")))
+ | false
+ => match Int.equal n 0 with
+ | true => []
+ | false
+ => match ls with
+ | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.firstn")))
+ | x :: xs
+ => x :: firstn (Int.sub n 1) xs
+ end
+ end
+ end.
+
+Ltac2 rec skipn (n : int) (ls : 'a list) :=
+ match Int.lt n 0 with
+ | true => Control.zero (Invalid_argument (Some (Message.of_string "List.skipn")))
+ | false
+ => match Int.equal n 0 with
+ | true => ls
+ | false
+ => match ls with
+ | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.skipn")))
+ | x :: xs
+ => skipn (Int.sub n 1) xs
+ end
+ end
+ end.
+
+Ltac2 rec nodup (eqb : 'a -> 'a -> bool) (ls : 'a list) :=
+ match ls with
+ | [] => []
+ | x :: xs
+ => match mem eqb x xs with
+ | true => nodup eqb xs
+ | false => x :: nodup eqb xs
+ end
+ end.
+
+(* seq start 1 last = start :: start + 1 :: ... :: (last - 1) *)
+Ltac2 rec seq (start : int) (step : int) (last : int) :=
+ match Int.lt (Int.sub last start) step with
+ | true
+ => []
+ | false
+ => start :: seq (Int.add start step) step last
+ end.
+
+Ltac2 init (len : int) (f : int -> 'a) :=
+ match Int.lt len 0 with
+ | true => Control.zero (Invalid_argument (Some (Message.of_string "List.init")))
+ | false => map f (seq 0 1 len)
+ end.
+
+Ltac2 repeat (x : 'a) (n : 'int) :=
+ init n (fun _ => x).
+
+Ltac2 assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) :=
+ let eq_key kv := let (k', _) := kv in eqk k k' in
+ let (_, v) := find eq_key l in
+ v.
+
+Ltac2 assoc_opt (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) :=
+ let eq_key kv := let (k', _) := kv in eqk k k' in
+ match find_opt eq_key l with
+ | Some kv => let (_, v) := kv in Some v
+ | None => None
+ end.
+
+Ltac2 mem_assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) :=
+ let eq_key kv := let (k', _) := kv in eqk k k' in
+ existsb eq_key l.
+
+Ltac2 remove_assoc (eqk : 'k -> 'k -> bool) (k : 'k) (l : ('k * 'v) list) :=
+ let eq_key kv := let (k', _) := kv in eqk k k' in
+ filter_out eq_key l.
+
+
+Ltac2 rec split (ls : ('a * 'b) list) :=
+ match ls with
+ | [] => ([], [])
+ | xy :: tl
+ => let (x, y) := xy in
+ let (left, right) := split tl in
+ ((x::left), (y::right))
+ end.
+Ltac2 rec combine (ls1 : 'a list) (ls2 : 'b list) :=
+ match ls1 with
+ | []
+ => match ls2 with
+ | [] => []
+ | _ :: _ => Control.zero (Invalid_argument (Some (Message.of_string "List.combine")))
+ end
+ | x :: xs
+ => match ls2 with
+ | y :: ys
+ => (x, y) :: combine xs ys
+ | [] => Control.zero (Invalid_argument (Some (Message.of_string "List.combine")))
+ end
+ end.
+
+Ltac2 enumerate (ls : 'a list) :=
+ combine (seq 0 1 (length ls)) ls.
+
+(* from Coq stdlib *)
+Ltac2 rec merge (cmp : 'a -> 'a -> int) (l1 : 'a list) (l2 : 'b list) :=
+ let rec merge_aux l2 :=
+ match l1 with
+ | [] => l2
+ | a1 :: l1'
+ => match l2 with
+ | [] => l1
+ | a2 :: l2'
+ => match Int.le (cmp a1 a2) 0 with
+ | true => a1 :: merge cmp l1' l2
+ | false => a2 :: merge_aux l2'
+ end
+ end
+ end in
+ merge_aux l2.
+
+Ltac2 rec merge_list_to_stack cmp stack l :=
+ match stack with
+ | [] => [Some l]
+ | l' :: stack'
+ => match l' with
+ | None => Some l :: stack'
+ | Some l'
+ => None :: merge_list_to_stack cmp stack' (merge cmp l' l)
+ end
+ end.
+
+Ltac2 rec merge_stack cmp stack :=
+ match stack with
+ | [] => []
+ | l :: stack'
+ => match l with
+ | None => merge_stack cmp stack'
+ | Some l => merge cmp l (merge_stack cmp stack')
+ end
+ end.
+
+Ltac2 rec iter_merge cmp stack l :=
+ match l with
+ | [] => merge_stack cmp stack
+ | a::l' => iter_merge cmp (merge_list_to_stack cmp stack [a]) l'
+ end.
+
+Ltac2 sort cmp l := iter_merge cmp [] l.
+
+(* TODO: maybe replace this with a faster implementation *)
+Ltac2 sort_uniq (cmp : 'a -> 'a -> int) (l : 'a list) :=
+ let rec uniq l :=
+ match l with
+ | [] => []
+ | x1 :: xs
+ => match xs with
+ | [] => x1 :: xs
+ | x2 :: _
+ => match Int.equal (cmp x1 x2) 0 with
+ | true => uniq xs
+ | false => x1 :: uniq xs
+ end
+ end
+ end in
+ uniq (sort cmp l).
diff --git a/user-contrib/Ltac2/Option.v b/user-contrib/Ltac2/Option.v
new file mode 100644
index 0000000000..0f09a0cc48
--- /dev/null
+++ b/user-contrib/Ltac2/Option.v
@@ -0,0 +1,27 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+Require Import Ltac2.Init.
+
+Ltac2 map (f : 'a -> 'b) (x : 'a option) :=
+ match x with
+ | Some x => Some (f x)
+ | None => None
+ end.
+
+Ltac2 bind (x : 'a option) (f : 'a -> 'b option) :=
+ match x with
+ | Some x => f x
+ | None => None
+ end.
+
+Ltac2 ret (x : 'a) := Some x.
+
+Ltac2 lift (f : 'a -> 'b) (x : 'a option) := map f x.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:20:38 +0000