commit: 353f4d2e9e4b7b42f2aed545165b298df689814e

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

Sun Oct 25 04:30:40 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Sun Oct 25 04:30:40 2026 +0000
tree: 7c1f5d7ca67c5b1ac1a08c804a9cbdec2b2daece
parent: 470a283711f8991fdd94fea56adebc8567e23c62 [diff]

perf: read `has_univ_param` and `get_loose_bvar_range` from the stored `Expr.data`

This PR makes the kernel read `has_univ_param` and `get_loose_bvar_range` from the data word stored in each expression, as `hash` and `has_fvar` already do, instead of calling into Lean.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

2 files changed

tree: 7c1f5d7ca67c5b1ac1a08c804a9cbdec2b2daece

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.