/lean4-ascii

Primary LanguageLeanApache License 2.0Apache-2.0

Lean 4 / ASCII

ASCII support for Lean 4.

Installation

Add this dependency to your project's lakefile.lean:

require ASCII from git "https://github.com/fgdorais/lean4-ascii" @ "main"

Then add import ASCII at the top of any Lean file where you plan to use this library.

  • The ASCII library is copyright © 2023 François G. Dorais. The library is released under the Apache 2.0 license. See the file LICENSE for additional details.