package coq-coinduction

  1. Overview
  2. No Docs
A library and plugin for doing proofs by (enhanced) coinduction

Install

Dune Dependency

Authors

Maintainers

Sources

v1.6.tar.gz
sha512=dd1ef575fe02377d21f13ceedbc102301164fb9f2c091cedeb6d1cd5b5d24d0d521919fac62c2f37f8b1cf249f8f5d37f9ce78ab886c8f834ee98c353dc558c3

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.

Dependencies (2)

  1. coq >= "8.16"
  2. ocaml

Dev Dependencies

None

Used by (1)

  1. coq-coinduction-examples < "1.7"

Conflicts

None