commit: 20e689217bc9d390b62168809606e995a19f04fa

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

Tue Mar 05 18:12:11 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Tue Mar 05 18:15:35 2024 -0800
tree: c27b67d20c7d09e2aa720016e1d94befe580abe4
parent: 65867d01e4a1d83b2a9cdaf73fabea46cb58e54b [diff]

refactor: `LinearArith/Nat/Basic.lean`

Motivation: avoid the unfold and check idiom.

closes #2615

src/Lean/Expr.lean[diff]
src/Lean/Meta/NatInstTesters.lean[Added - diff]
src/Lean/Meta/Offset.lean[diff]
src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean[diff]
tests/lean/run/2615.lean[Added - diff]

5 files changed

tree: c27b67d20c7d09e2aa720016e1d94befe580abe4

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.