coq-monae.opam

# This file was generated from `meta.yml`, please do not edit manually.
# Follow the instructions on https://github.com/coq-community/templates to regenerate.

opam-version: "2.0"
maintainer: "Reynald Affeldt <reynald.affeldt@aist.go.jp>"
version: "dev"

homepage: "https://github.com/affeldt-aist/monae"
dev-repo: "git+https://github.com/affeldt-aist/monae.git"
bug-reports: "https://github.com/affeldt-aist/monae/issues"
license: "LGPL-2.1-or-later"

synopsis: "Monads and equational reasoning in Coq"
description: """
This Coq library contains a hierarchy of monads with their laws used
in several examples of monadic equational reasoning."""

build: [make "-j%{jobs}%" ]
install: [make "install_full"]
depends: [
  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
  "coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev")  }
  "coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev")  }
  "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev")  }
  "coq-mathcomp-solvable" { (>= "2.2.0") | (= "dev")  }
  "coq-mathcomp-field" { (>= "2.2.0") | (= "dev")  }
  "coq-mathcomp-analysis" { (>= "1.5.0")}
  "coq-infotheo" { >= "0.7.3"}
  "coq-paramcoq" { >= "1.1.3" & < "1.2~" }
  "coq-hierarchy-builder" { >= "1.5.0" }
  "coq-equations" { >= "1.3" & < "1.4~" }
]

tags: [
  "keyword:monae"
  "keyword:effects"
  "keyword:probability"
  "keyword:nondeterminism"
  "logpath:monae"
]
authors: [
  "Reynald Affeldt"
  "David Nowak"
  "Takafumi Saikawa"
  "Jacques Garrigue"
  "Ayumu Saito"
  "Celestine Sauvage"
  "Kazunari Tanaka"
]