commit: 191a7bf2c0169b6e312f3c5f0c551a5312ebe578

[log]
author: Kyle Miller <kmill31415@gmail.com>

Sat May 16 14:51:36 2026 -0700
committer: Kyle Miller <kmill31415@gmail.com>

Thu May 21 07:33:39 2026 -0700
tree: a682c2a1458c90e1f5fca61badfa87a7330676a6
parent: 727b4aad2bbb2562e0e2b42e29334738409d167c [diff]

feat: improve performance of structure instance notation elaboration

This PR improves elaboration performance for structure instance notation by substituting fields into types as needed.

src/Lean/Elab/StructInst.lean[diff]

1 file changed

tree: a682c2a1458c90e1f5fca61badfa87a7330676a6

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.