package coq-lean-import

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

Install

Dune Dependency

Authors

Maintainers

Sources

v9.0-lean3+alpha.tar.gz
sha512=2f49766d0b667d897b5a62b4806db129967c717ad0a15d484da6c29ee77e85a918188ffa4cb0372c320ea6563df1a5e8273f9d2e7c8745c220c5aa2b3f7bf9fa

Description

Plugin allowing Coq to import Lean exported files.

Tags

logpath:LeanImport

Published: 28 Aug 2025

Dependencies (2)

  1. coq >= "9.0" & < "9.1~"
  2. ocaml >= "4.09.0"

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover