package rocq-lean-import

  1. Overview
  2. Homepage
Plugin allowing Rocq to import Lean exported files

Install

Dune Dependency

Authors

Maintainers

Sources

v0.0.2.tar.gz
sha512=bd50f013f4fa6885755d2d4ba619408da3c0e58c94b1176b7d873c3be3f4b488d15c6e5b52cde31cc9533801265940051d2b95aac5380a14e87d4489e8324c8d

Description

Plugin allowing Rocq to import Lean exported files.

Tags

logpath:LeanImport

Published: 27 May 2026

Dependencies (3)

  1. rocq-stdlib
  2. rocq-core >= "9.2~" & < "9.3~"
  3. ocaml >= "4.09.0"

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover