package coq-higman-cf
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
A direct constructive proof of Higman's Lemma
Install
Dune Dependency
Authors
Maintainers
Sources
v8.5.0.tar.gz
md5=d7aa48da8599c6f16969e195bf7c61e0
Description
This development formalizes in Coq the Coquand-Friedlender proof of Higman's lemma for a two-letter alphabet. An efficient program can be extracted from the proof.
On This Page