Optimize DomainTheory imports and repeated proofs

d8a4e4a

Select commit

Loading

Failed to load commit list.

Uh oh!

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

Greptile Apps

Greptile Review

Project Advisory Comment on: pull_request_target 3

Project metadata advisory

Workflow Lint on: pull_request 1

scope

actionlint

SHA-pinned Actions

Python CI on: pull_request 1

scope

Lint (ruff)

Test (pytest)

Partial Port Audit on: pull_request 2

audit (advisory)

Lean Action CI on: pull_request 5

Plan build

Build pool

Build shard ${{ matrix.shard }}

Check rebased root

Assemble and lint

Build project

Documentation on: pull_request 1

scope

Documentation preflight

Proof Profile on: pull_request 11

Plan profile

Measure base 00

Measure base 01

Measure head 00

Measure head 01

Profile added files

Report profile

PR Separation Guard on: pull_request 1

Content / non-content separation

Exposition Verify on: pull_request 1

scope

build-ready

Verify minimal Lean files

Greptile Apps / Greptile Review succeeded Oct 25, 2026 in 4m 4s

Base review

Greptile has reviewed the Pull Request.

127 files reviewed, 1 comments added.

View more details on Greptile Apps

Loading

Re-running checks...