package rocq-sulfur

You can search for identifiers within the package.

in-package search v0.2.0

A Rocq plugin to automate reasoning about languages with binders

Install

Dune Dependency

github.com Edit opam file Versions (1)

Authors

Maintainers

T

Théo Winterhalter <theo.winterhalter@inria.fr>

Sources

v0.1.tar.gz

md5=a9300a89e90327b1c282d05ea6c9565b

sha512=09364007f26ac1560d73a9d99610b8d136da52fa9d3cf2c0b8e290e8ce8752998f98208813aed495e2cabea10bf6c36cb0e6d44d9f1a5b331f79d92b89dc99cc

Description

Sulfur generates, from a signature, the syntax of a language with binders together with renaming, substitution, and a tactic (ssimpl) that normalises terms and substitutions.

Published: 23 Oct 2026

Dependencies (4)

rocq-equations
rocq-stdlib
rocq-core >= "9.3.0" & < "9.4~"
dune >= "3.21"

Dev Dependencies (1)

odoc with-doc

Used by

None

Conflicts