package coq-catt-plugin

You can search for identifiers within the package.

in-package search v0.2.0

A Coq plugin for the catt proof-assistant

Install

Dune Dependency

github.com Readme Changelog MIT License Edit opam file Versions (1)

Authors

Maintainers

Sources

sha256=20a0b4aae3655274cb7336cb158699ceb1ee29909e50405d0ccb9d54d985baeb

sha512=1919da8eea60817a0907be4aa6f399a9e66fc8746d190ea805de8721a44f5f8a68b9c67626b7767e42a7cd0f061e00c16cd6c63570cbdedf15bc31f8b598f72b

CHANGES.md.html

1.0 (2024-10)

Coq catt plugin

Working export of catt term into coq

Catt

Computation of 1-naturality
Computation of functorialisation
Computation of inverses and cancellation witnesses
Computation of opposites
Builtin identities and compositions
Computation of suspension and implicit suspension
Inference of implicit variables
Basic type checker