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.8.0.tar.gz
md5=b6510a832128ef667bfabad1dac3529c
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