commit: 4c439c73a7473ec51ac0763f15bd6e53dcbaff0f

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

Sun Sep 15 17:45:39 2024 +0200
committer: GitHub <noreply@github.com>

Sun Sep 15 15:45:39 2024 +0000
tree: d7baa4b1b23c148e50f0f3a27957e10e218bf48c
parent: 5eea8355baa64e6fda4e3874a0f45649d4c27633 [diff]

test: tracing and test case for #5347 (#5348)

not a fix, unfortunately, just recording the test.

src/Lean/Meta/Tactic/FunInd.lean[diff]
tests/lean/run/issue5347.lean[Added - diff]

2 files changed

tree: d7baa4b1b23c148e50f0f3a27957e10e218bf48c

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