commit: 5e64b6d846082f901eaa9e556952f2c1edc4523e

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

Sat Oct 12 15:00:30 2024 +0200
committer: Joachim Breitner <mail@joachim-breitner.de>

Sat Oct 12 15:00:30 2024 +0200
tree: 023e9c7c8d3508aadbedfe1697b0098baec86544
parent: b814be6d6a5334784b172db15fd7fea39b4e3233 [diff]

refactor: remove mkRecursorInfoForKernelRec

it seems to be unused, arguably even for kernel recursors their type
should be usable with `mkRecursorInfo`, and removing this will help
understand the impact of #5679.

src/Lean/Meta/RecursorInfo.lean[diff]

1 file changed

tree: 023e9c7c8d3508aadbedfe1697b0098baec86544

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