commit: 57cd1368c1afc0b7787e93598571ee5a17a015c8

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

Sat Nov 16 15:53:40 2024 -0800
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Nov 16 15:55:59 2024 -0800
tree: 4870751bba09401a7e1bef394d87679319bff6fe
parent: 9a8543347796e52070ff7936661ae48fcebfea60 [diff]

fix: circular assignment at structure instance elaborator

This PR fixes a stack overflow caused by a cyclic assignment in the
metavariable context. The cycle is unintentionally introduced by the
structure instance elaborator.

closes #3150

src/Lean/Elab/StructInst.lean[diff]
tests/lean/run/3150.lean[Added - diff]

2 files changed

tree: 4870751bba09401a7e1bef394d87679319bff6fe

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 (documentation source: doc/make/index.md).