coq-founify

Correctness and extraction of the unification algorithm. A notion of terms based on symbols without fixed arities is defined and an extended unification problem is proved solvable on these terms. An algorithm, close from Robinson algorithm, can be extracted from the proof.

opam install coq-founify.8.6.0
homepage
https://github.com/coq-contribs/founify
license
Unknown
bugs tracker
https://github.com/coq-contribs/founify/issues
dependencies
coq (>= 8.6 & < 8.7~)
source
https://github.com/coq-contribs/founify/archive/v8.6.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-founify/coq-founify.8.6.0