Put theorem headers on their own line after include/omit

4b1e37f

Select commit

Loading

Failed to load commit list.

Uh oh!

There was an error while loading. Please reload this page.

Greptile Apps

Greptile Review

Exposition Verify on: pull_request 1

scope

build-ready

Verify minimal Lean files

Python CI on: pull_request 1

scope

Lint (ruff)

Test (pytest)

Proof Profile on: pull_request 7

Plan profile

Measure base 00

Measure head 00

Profile added files

Report profile

Project Advisory Comment on: pull_request_target 3

Project metadata advisory

PR Separation Guard on: pull_request 1

Content / non-content separation

Lean Action CI on: pull_request 5

Plan build

Build pool

Build shard ${{ matrix.shard }}

Check rebased root

Assemble and lint

Build project

Workflow Lint on: pull_request 1

scope

actionlint

SHA-pinned Actions

Partial Port Audit on: pull_request 2

audit (advisory)

Documentation on: pull_request 1

scope

Documentation preflight

Greptile Apps / Greptile Review succeeded Nov 5, 2026 in 3m 25s

Base review

Greptile has reviewed the Pull Request.

12 files reviewed, 0 comments added.

View more details on Greptile Apps

Loading

Re-running checks...