add MonadTypedStore

.github/workflows/docker-action.yml

@@ -17,7 +17,9 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'mathcomp/mathcomp:1.16.0-coq-8.16'
           - 'mathcomp/mathcomp:1.16.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.16'
           - 'mathcomp/mathcomp:1.17.0-coq-8.17'
       fail-fast: false
     steps:

README.md

@@ -26,7 +26,7 @@ in several examples of monadic equational reasoning.
   - Celestine Sauvage
   - Kazunari Tanaka
 - License: [LGPL-2.1-or-later](LICENSE)
-- Compatible Coq versions: Coq 8.17
+- Compatible Coq versions: Coq 8.16-8.17
 - Additional dependencies:
   - [MathComp ssreflect](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)

_CoqProject

@@ -13,19 +13,22 @@ state_lib.v
 array_lib.v
 trace_lib.v
 proba_lib.v
+typed_store_lib.v
 monad_composition.v
 monad_model.v
 proba_monad_model.v
 category.v
 gcm_model.v
 altprob_model.v
 monad_transformer.v
+typed_store_model.v
 example_spark.v
 example_nqueens.v
 example_relabeling.v
 example_quicksort.v
 example_iquicksort.v
 example_monty.v
+example_typed_store.v
 smallstep.v
 example_transformer.v
 category_ext.v

coq-monae.opam

@@ -15,10 +15,10 @@ description: """
 This Coq library contains a hierarchy of monads with their laws used
 in several examples of monadic equational reasoning."""
 
-build: [make "-j%{jobs}%" ]
+build: [make "-j%{jobs}%"]
 install: [make "install_full"]
 depends: [
-  "coq" { (>= "8.17" & < "8.18~") | (= "dev") }
+  "coq" { (>= "8.16" & < "8.18~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "1.16.0" & < "1.18~") | (= "dev")  }
   "coq-mathcomp-fingroup" { (>= "1.16.0" & < "1.18~") | (= "dev")  }
   "coq-mathcomp-algebra" { (>= "1.16.0" & < "1.18~") | (= "dev")  }