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.7.0.tar.gz
md5=9dbdfa001becaadefaa6d2ebbf2ca644
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