package coq-lean-import

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

Install

Dune Dependency

Authors

Maintainers

Sources

v8.20-lean3+alpha.tar.gz
sha512=f8b7bbc6e4ce52e458ca7f2b48c30a5df1c63b1eb4a59a26fff0b7a96f1211298379972e6e799baad3205443e040de3a246e8b90efb266bb5d177e030ab57e25

Description

Plugin allowing Coq to import Lean exported files.

Tags

logpath:LeanImport

Published: 28 Aug 2025

Dependencies (2)

  1. coq >= "8.20" & < "8.21~"
  2. ocaml >= "4.09.0"

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover