coq-via-egg-plugin.opam

opam-version: "2.0"
maintainer: "kozyrev.andreiii2016@gmail.com"

homepage: "https://github.com/K-dizzled/relations-via-egg"
dev-repo: "git+https://github.com/K-dizzled/relations-via-egg.git"
bug-reports: "https://github.com/K-dizzled/relations-via-egg/issues"
doc: "https://github.com/K-dizzled/relations-via-egg"
license: "MIT"

synopsis: "COQ Plugin solving relations from Hahn coq lib using Rust EGG library"
description: """
A COQ plugin, designed for sloving relations from Hahn coq lib. The plugin uses OCaml <-> Rust foreign function interface to access Rust EGG library and then generates a proof in coq."""

build: ["dune" "build" "-p" name "-j" jobs]
depends: [
  "ocaml" {>= "4.07.1"}
  "dune" {>= "3.5"}
  "coq" {>= "8.16.0"}
  "coq-hahn" { >= "1.1" | (= "dev") }
  "coq-promising-lib" { = "dev" }
]

tags: [
  "category:Coq Extensions"
  "keyword:Equality Saturation"
  "logpath:CeggPlugin"
]

authors: [
  "Andrei Kozyrev"
]