commit: 799b2b662825e646609963921f2c68489b2e664a

[log]
author: Joachim Breitner <mail@joachim-breitner.de>

Mon Nov 18 12:28:02 2024 +0100
committer: GitHub <noreply@github.com>

Mon Nov 18 11:28:02 2024 +0000
tree: b0a0e2ab45a27f535128b589dcda1250c6fc87c4
parent: b8d6e44c4f65c9a38f2ebc8e2d1691575b53e761 [diff]

fix: handle reordered indices in structural recursion (#6116)

This PR fixes a bug where structural recursion did not work when indices
of the recursive argument appeared as function parameters in a different
order than in the argument's type's definition.

Fixes #6015.

4 files changed

tree: b0a0e2ab45a27f535128b589dcda1250c6fc87c4

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).