commit: 9e2440bf56ef259ecd0b5400c5e16cd3fb35e885

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

Mon Mar 04 15:32:02 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Mon Mar 04 15:33:11 2024 -0800
tree: e62cf612f8e90f05217bd436e9986b366c968d5e
parent: e814fc859e8feb2c7e1c94a1d8b05e8b27149e62 [diff]

fix: bug at `elimOptParam`

`let_expr` uses `cleanupAnnotations` which consumes `optParam` type annotations.

src/Lean/Meta/Injective.lean[diff]
tests/lean/run/elimOptParam.lean[Added - diff]

2 files changed

tree: e62cf612f8e90f05217bd436e9986b366c968d5e

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.