Skip to content

Actions: leanprover/lean4

Actions

Restart by label

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
restart-on-label.yml
6,920 workflow runs
6,920 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

perf: de-fuel some recursive definitions in Core Restart by label #8256: Pull request #11416 unlabeled by leanprover-community-bot
Skipped
Skipped
perf: when matching on values, avoid generating hyps when not needed Restart by label #8255: Pull request #11508 labeled by nomeata
1s
1s
perf: de-fuel some recursive definitions in Core Restart by label #8254: Pull request #11416 unlabeled by nomeata
1s
1s
perf: de-fuel some recursive definitions in Core Restart by label #8253: Pull request #11416 labeled by nomeata
1s
1s
feat: proper recursive specialization Restart by label #8252: Pull request #11479 labeled by leanprover-community-bot
1s
1s
feat: proper recursive specialization Restart by label #8251: Pull request #11479 labeled by leanprover-bot
1s
1s
perf: avoid double-open per .olean file Restart by label #8250: Pull request #11507 labeled by Kha
1s
1s
feat: remove Finite conditions from iterator consumers relying on a new fixpoint combinator Restart by label #8249: Pull request #11038 labeled by leanprover-bot
1s
1s
feat: remove Finite conditions from iterator consumers relying on a new fixpoint combinator Restart by label #8248: Pull request #11038 labeled by datokrat
Skipped
Skipped
feat: remove Finite conditions from iterator consumers relying on a new fixpoint combinator Restart by label #8247: Pull request #11038 labeled by datokrat
7s
7s
chore: use not_value at Nat.pow_pos Restart by label #8246: Pull request #11523 labeled by leodemoura
2s
2s
feat: grind propagators for Nat operators Restart by label #8245: Pull request #11522 labeled by leodemoura
1s
1s
fix: segmentation fault that was triggered when initializing a new timer and a reset was called at the same time Restart by label #8244: Pull request #11521 labeled by algebraic-dev
1s
1s
feat: add not_value constraint to grind_pattern Restart by label #8243: Pull request #11520 labeled by leodemoura
1s
1s
feat: mark Nat power and divisibility theorems for grind Restart by label #8242: Pull request #11519 labeled by leodemoura
1s
1s
feat: hint when an autobound variable's type fails to be a function Restart by label #8241: Pull request #11518 labeled by robsimmons
Skipped
Skipped
feat: constant folding for Nat.mul Restart by label #8240: Pull request #11517 labeled by hargoniX
6s
6s
feat: exact? uses star-indexed lemmas as fallback Restart by label #8239: Pull request #11494 labeled by kim-em
1s
1s
refactor: lake: disambiguate packages by workspace index Restart by label #8238: Pull request #11500 labeled by leanprover-bot
1s
1s
fix: find? -> findRev? Restart by label #8237: Pull request #11514 labeled by leanprover-community-bot
1s
1s
feat: simpler error message when sorries complicate universe inference Restart by label #8236: Pull request #11513 labeled by robsimmons
1s
1s
fix: find? -> findRev? Restart by label #8235: Pull request #11514 labeled by leanprover-bot
1s
1s
refactor: move Std.Range to Std.Legacy.Range Restart by label #8234: Pull request #11438 labeled by leanprover-community-bot
1s
1s
refactor: move Std.Range to Std.Legacy.Range Restart by label #8233: Pull request #11438 labeled by leanprover-bot
1s
1s
feat: lint coercions that are deprecated or banned in core Restart by label #8232: Pull request #11511 labeled by leanprover-community-bot
1s
1s