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.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.
Tags
keyword:coinduction keyword:up to techniques keyword:companion logpath:CoinductionPublished: 08 Sep 2022
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page