commit: 0eea1e4f35244e5a39adf9fe3edc65e3c6317598

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

Wed Dec 24 18:15:18 2025 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Wed Dec 24 18:16:44 2025 -0800
tree: bf89505af08d4809d4a0b68262f7e0155d86d4fa
parent: 723acce2a7179cd0f3ebb7deb833528cb6226fef [diff]

feat: add `Sym.getMaxFVar?`

This PR adds the function `getMaxFVar?` for implementing `SymM` primitives.

src/Lean/Meta/Sym.lean[diff]
src/Lean/Meta/Sym/Main.lean[diff]
src/Lean/Meta/Sym/MaxFVar.lean[Added - diff]
src/Lean/Meta/Sym/SymM.lean[diff]
tests/lean/run/getMaxFVar.lean[Added - diff]

5 files changed

tree: bf89505af08d4809d4a0b68262f7e0155d86d4fa

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.