[Ltac2] Add util files for Bool, List, Option

Most functions are taken either from the Coq standard library or the
OCaml standard library.  One (`enumerate`) is taken from Python.  Most
names are chosen according to OCaml conventions (as Coq does not have
exceptions, and so the OCaml naming conventions already distinguish
between option and exception).  Since `exists` is a keyword, we use the
Coq name `existsb` instead.  We generally favor Coq argument ordering
when there is a conflict between Coq and OCaml.

Note that `seq` matches neither Coq nor OCaml; it takes a `step`
argument for how much to increment by on each step.

Sorting functions are mostly taken from Coq's mergesort library; it
might make sense to replace them with OCaml's versions for efficiency?

1 files changed, 63 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.