From 7ed97ca4790c1ddc5a0cfec18d587704aab49c4b Mon Sep 17 00:00:00 2001
From: Julin S <famubu@rawtext.club>
Date: Fri, 20 Oct 2023 12:12:22 +0530
Subject: [PATCH] [ocaml] try a monad module type

---
 coq/mathcomp/mathcomp2/_CoqProject | 11 +++++++++++
 ocaml/monads.ml                    | 16 ++++++++++++++++
 2 files changed, 27 insertions(+)
 create mode 100644 coq/mathcomp/mathcomp2/_CoqProject
 create mode 100644 ocaml/monads.ml

diff --git a/coq/mathcomp/mathcomp2/_CoqProject b/coq/mathcomp/mathcomp2/_CoqProject
new file mode 100644
index 0000000..6b4592f
--- /dev/null
+++ b/coq/mathcomp/mathcomp2/_CoqProject
@@ -0,0 +1,11 @@
+-I /media/julinusername/eins/gits/math-comp/mathcomp
+-R /media/julinusername/eins/gits/math-comp/mathcomp mathcomp
+
+-arg -w -arg -projection-no-head-constant
+-arg -w -arg -redundant-canonical-projection
+-arg -w -arg -notation-overridden
+-arg -w -arg +duplicate-clear
+-arg -w -arg +non-primitive-record
+-arg -w -arg +undeclared-scope
+-arg -w -arg +deprecated-hint-rewrite-without-locality
+-arg -w -arg -elpi.add-const-for-axiom-or-sectionvar
diff --git a/ocaml/monads.ml b/ocaml/monads.ml
new file mode 100644
index 0000000..9e1449e
--- /dev/null
+++ b/ocaml/monads.ml
@@ -0,0 +1,16 @@
+(* https://cs3110.github.io/textbook/chapters/ds/monads.html *)
+
+module type Monad = sig
+  type 'a t
+  val return: 'a -> 'a t
+  val (>>=): 'a t -> ('a -> 'b t) -> 'b t
+end
+
+module Maybe : Monad = struct
+  type 'a t = 'a option
+  let return a = Some a
+  let (>>=) a f =
+    match a with
+    | None -> None
+    | Some a' -> f a'
+end