package coq-rewriter

  1. Overview
  2. Homepage
Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography

Install

Dune Dependency

Authors

Maintainers

Sources

v0.0.21.tar.gz
sha512=f236b711d04bc21359cbf7e4c4bf3789a0f816630a573c6ba6bdac3cc4ed9c17924d121e40f820f9c9f0cec8c0fef02c9947013bfd0f40b47d7843edf773c9bb

Description

Tags

logpath:Rewriter

Published: 11 Sep 2026

Dependencies (3)

  1. coq >= "8.19~"
  2. ocaml build & (arch = "x86_32" | arch = "x86_64" | >= "4.14.0")
  3. conf-findutils build

Dev Dependencies

None

Used by (1)

  1. coq-fiat-crypto >= "0.1.2"

Conflicts

None

Rocq

Interactive Theorem Prover