commit: 8ab452c9919a04ba33e2e9d52710ab9fb36524a3

[log]
author: Kim Morrison <kim@tqft.net>

Mon Mar 02 23:57:53 2026 +0000
committer: Kim Morrison <kim@tqft.net>

Mon Mar 02 23:57:53 2026 +0000
tree: f288217b79a597b206abd7d167e140e7d688e06f
parent: 04ccf7cb2800b2073dc999ea511d5afc3f77133c [diff]

fix: delete empty .out.expected files instead of leaving them empty

The lint.sh check flags empty .out.expected files. Delete them entirely
since these tests no longer produce expected output.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

tests/elab/1132.lean.out.expected[Deleted - diff]
tests/elab/casesRec.lean.out.expected[Deleted - diff]

2 files changed

tree: f288217b79a597b206abd7d167e140e7d688e06f

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.