commit: 8cbaa1cd30fae02a01a63fb5b90bff182356a4d8

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

Sun Sep 22 17:40:55 2024 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Sun Sep 22 17:51:43 2024 -0700
tree: 8212d4abbd1cc2b2ecafeedfea899e54f856cd7b
parent: a6830f90ab365e14ccb7ca31201de37f8c1e978c [diff]

fix: must not reduce `ite` in the discriminant of match-expression when reducibility setting is `.reducible`

closes #5388

5 files changed

tree: 8212d4abbd1cc2b2ecafeedfea899e54f856cd7b

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).