commit: ea9fad0706f0b1da2467195dae75480595640670

[log]
author: Robin Arnez <152706811+Rob23oba@users.noreply.github.com>

Sat Aug 01 11:28:03 2026 +0200
committer: GitHub <noreply@github.com>

Sat Aug 01 09:28:03 2026 +0000
tree: fb8e6dddf9e75bf77e4aaeefd7562eb56e179f65
parent: 23393b959b33e3a8d15796b2397f8a04c315b9f4 [diff]

chore: remove deprecated `toCtorIdx` alias for `ctorIdx` (#14627)

This PR removes `toCtorIdx` which has been deprecated for almost a year
by now.

2 files changed

tree: fb8e6dddf9e75bf77e4aaeefd7562eb56e179f65

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.