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.4.tar.gz
sha512=6c82abfc6db1d0d51473d298037681cdae3e2a3a8090e00ad124f517314ca209ba3109fb853487de0f8b6511b293b940c8292e12124072131864b368c387fcb6
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: 30 Mar 2022
On This Page