Artifact

CanonicalLean Software

Author Chase Norman

Part of: Collection: Supplementary Materials
License: MIT License
Publication Date: 2025-09-22

Document Identifiers

DOI: 10.4230/artifacts.24708
URN: urn:nbn:de:0030-drops-247085

Author Details

Chase Norman

Carnegie Mellon University

Content

Software: https://github.com/chasenorman/CanonicalLean
archived version

Version/Status

Content created at: 2025-04-10
Status: Active (at the time of publication 2025-09-22)

Cite As Get BibTex

Chase Norman. CanonicalLean (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/artifacts.24708

Description

The canonical tactic proves theorems, synthesizes programs, and constructs objects in Lean.

Subject Classification

Keywords

dependent types
theorem proving
program synthesis
formal methods
theorem prover
automated reasoning
lean4

Programming Languages

Lean

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

Metadata Views

Questions / Remarks / Feedback

X

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail

© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact