package coq-coinduction

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

Install

Dune Dependency

github.com Edit opam file Versions (11)

Authors

  1. D
    Damien Pous

Maintainers

  1. D
    damien.pous@ens-lyon.fr

Sources

v1.3.tar.gz
sha512=8ba44865cde1bd882541556db666200376900b175388b2889f81053be3f5d4c695a3d28ae6c5eca307a7430e255213e7544472c71e35c2c708a8df045f952289

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.

Tags

keyword:coinduction keyword:up to techniques keyword:companion logpath:Coinduction

Published: 29 Oct 2021

Dependencies (2)

  1. coq >= "8.13" & < "8.15~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None