package coq-coinduction
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
A library and plugin for doing proofs by (enhanced) coinduction
Install
Dune Dependency
Authors
Maintainers
Sources
v1.2.tar.gz
sha512=69112fac78d6f7205ad529fe7d397d87543ed165694b46c20eea77f7050fbec8cb05071dd294223c8fe93517ec56b70b7312685292bba2e9de8fde6bccabebe4
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:CoinductionPublished: 08 Oct 2021
On This Page