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.9.0.tar.gz
md5=1ce02b6135e92838aaf98fc5932274bf
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