coinduction/rocq-coinduction.opam at master · damien-pous/coinduction · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
opam-version: "2.0"
maintainer: "damien.pous@ens-lyon.fr"
version: "8.20.dev"

homepage: "https://github.com/damien-pous/coinduction"
dev-repo: "git+https://github.com/damien-pous/coinduction.git"
bug-reports: "https://github.com/damien-pous/coinduction/issues"
license: "GNU LGPL"

synopsis: "A library for doing proofs by (enhanced) coinduction"
description: """
Coinductive predicates are greatest fixpoints of monotone functions.
The `companion' makes it possible to enhance the associated coinduction scheme.
This library provides a formalisation on enhancements based on the companion, as well as tactics in making it straightforward to perform proofs by enhanced coinduction.
"""

build: [
  [make "-j%{jobs}%" ]
]
install: [make "install"]
depends: [
  "rocq-prover" {>= "9.0.0"}
  "rocq-stdlib"
]

tags: [
  "keyword:coinduction"
  "keyword:up to techniques"
  "keyword:companion"
  "keyword:bisimilarity"
  "logpath:Coinduction"
]
authors: [
  "Damien Pous"
]