coq-fitch.opam

opam-version: "2.0"
maintainer: "palmskog@gmail.com"
version: "dev"

homepage: "https://github.com/palmskog/fitch"
dev-repo: "git+https://github.com/palmskog/fitch.git"
bug-reports: "https://github.com/palmskog/fitch/issues"
license: "MIT"

synopsis: "Sound Fitch-style proof system in Coq for propositional logic"
description: """
A certified proof system and checker in Coq for Fitch-style propositional logic,
as defined in the book Logic for Computer Science by Huth and Ryan.
The checker is both executable inside Coq and after extraction to OCaml code.
"""

build: ["dune" "build" "-p" name "-j" jobs]
depends: [
  "dune" {>= "2.5"}
  "coq" {>= "8.16"}
  "coq-ott" {>= "0.33"}
]

tags: [
  "category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures"
  "keyword:proof system"
  "keyword:propositional logic"
  "logpath:Fitch"
]
authors: [
  "Karl Palmskog"
]