InfSeqExt/coq-inf-seq-ext.opam at master · DistributedComponents/InfSeqExt · 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
opam-version: "2.0"
maintainer: "palmskog@gmail.com"
version: "dev"

homepage: "https://github.com/DistributedComponents/InfSeqExt"
dev-repo: "git+https://github.com/DistributedComponents/InfSeqExt.git"
bug-reports: "https://github.com/DistributedComponents/InfSeqExt/issues"
license: "Unknown"

synopsis: "Coq library for reasoning inductively and coinductively on infinite sequences"
description: """
Coq library for reasoning inductively and coinductively on infinite sequences,
using modal operators similar to those in linear temporal logic (LTL)."""

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

tags: [
  "category:Mathematics/Logic/Modal logic"
  "keyword:temporal logic"
  "keyword:infinite transition systems"
  "keyword:coinduction"
  "logpath:InfSeqExt"
]
authors: [
  "Yuxin Deng"
  "Jean-Francois Monin"
  "Karl Palmskog"
  "Ryan Doenges"
]