leanprover/lean2

Lean theorem prover version 0.2 (it supports standard and HoTT modes)

C++

128

8,019 commits

updated Mar 19, 2022

README

This is a snapshot of the Lean 0.2 theorem prover. We have this separate repository because this version has special support for Homotopy Type Theory.

About

Requirements

C++11 compatible compiler: g++ (version >= 4.8.1), or clang++ (version >= 3.3)
CMake
GMP (GNU multiprecision library)
MPFR (GNU MPFR Library)
Lua 5.2 or 5.1, or LuaJIT 2.0

Installing

Windows

MSys2

Linux

OS X

OS X 10.9

Build Instructions

Miscellaneous

Building Doxygen Documentation: doxygen src/Doxyfile
Coding Style
Library Style Conventions
Git Commit Conventions
Syntax Highlight Lean Code in LaTeX

Contributors

6,567 commits

830 commits

385 commits

89 commits

Similar repos

leanprover/lean

Lean Theorem Prover

2,154

same org

leanprover/tutorial

Lean Tutorials

same org

leanprover/theorem_proving_in_lean

Theorem proving in Lean

same org

leanprover/lean3-mode

Emacs mode for Lean

same org

leanprover/elan

The Lean version manager

637

same org

leanprover/theorem_proving_in_lean4

Theorem Proving in Lean 4

275

same org

leanprover/tc

Reference type checker for the Lean theorem prover

same org

leanprover/lean4

Lean 4 programming language and theorem prover

9,248

same org

Languages

C++

50.8%

Lean

44.3%

Emacs Lisp

2.2%

leanprover/lean2

Lean theorem prover version 0.2 (it supports standard and HoTT modes)

C++

128

8,019 commits

updated Mar 19, 2022

See the code

README

This is a snapshot of the Lean 0.2 theorem prover. We have this separate repository because this version has special support for Homotopy Type Theory.