commit: 36cf33747592a1b9b9ff15c784ae5994ed851349

[log]
author: Leonardo de Moura <leomoura@amazon.com>

Tue Dec 03 14:45:59 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Tue Dec 03 14:46:54 2024 -0800
tree: ac1bbb6356e75bf9c531b6bf6197b66964f9d892
parent: 12af1aa1233212a99e0a94555aa28a964f1ab71c [diff]

fix: ensure `sorry` is available

We want to make sure we can use `debug.proofAsSorry` when compiling Lean.

src/Lean/Elab/MutualDef.lean[diff]

1 file changed

tree: ac1bbb6356e75bf9c531b6bf6197b66964f9d892

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).