Skip to content

Actions: leanprover/lean4

Actions

Label PR based on Comment

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
labels-from-comments.yml
6,748 workflow runs
6,748 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

feat: localize universe metavariable errors at let bindings and fun binders Label PR based on Comment #6753: Issue comment #5402 (comment) created by leanprover-community-bot
September 21, 2024 18:48 2s
September 21, 2024 18:48 2s
feat: qsort with proven bounds and correctness proof Label PR based on Comment #6752: Issue comment #5346 (comment) created by lyphyser
September 21, 2024 17:04 2s
September 21, 2024 17:04 2s
feat: expose Kernel.check for debugging purposes Label PR based on Comment #6751: Issue comment #5412 (comment) created by leanprover-community-bot
September 21, 2024 11:12 2s
September 21, 2024 11:12 2s
Hovering over underscore (_) shows type, but not term Label PR based on Comment #6750: Issue comment #5367 (comment) created by thorimur
September 21, 2024 01:19 2s
September 21, 2024 01:19 2s
feat: BitVec.toNat_{add,sub,mul_of_lt} for BitVector non-overflow reasoning Label PR based on Comment #6749: Issue comment #5411 (comment) created by bollu
September 20, 2024 21:27 2s
September 20, 2024 21:27 2s
fix: downgrade instance synth order issues to warnings Label PR based on Comment #6748: Issue comment #5399 (comment) created by digama0
September 20, 2024 20:34 2s
September 20, 2024 20:34 2s
fix: downgrade instance synth order issues to warnings Label PR based on Comment #6747: Issue comment #5399 (comment) created by kmill
September 20, 2024 20:30 2s
September 20, 2024 20:30 2s
feat: localize universe metavariable errors at let bindings and fun binders Label PR based on Comment #6746: Issue comment #5402 (comment) created by kmill
September 20, 2024 20:21 2s
September 20, 2024 20:21 2s
feat: BitVec.toNat_{add,sub,mul_of_lt} for BitVector non-overflow reasoning Label PR based on Comment #6745: Issue comment #5411 (comment) created by tobiasgrosser
September 20, 2024 19:58 2s
September 20, 2024 19:58 2s
fix: downgrade instance synth order issues to warnings Label PR based on Comment #6744: Issue comment #5399 (comment) created by TomasPuverle
September 20, 2024 18:12 2s
September 20, 2024 18:12 2s
feat: BitVec.toNat_{add,sub,mul_of_lt} for BitVector non-overflow reasoning Label PR based on Comment #6743: Issue comment #5411 (comment) created by leanprover-community-mathlib4-bot
September 20, 2024 17:19 2s
September 20, 2024 17:19 2s
feat: BitVec analogues of Nat.{mul_two, two_mul, mul_succ, succ_mul} Label PR based on Comment #6742: Issue comment #5410 (comment) created by leanprover-community-mathlib4-bot
September 20, 2024 15:57 2s
September 20, 2024 15:57 2s
Please make installing LICENSE and LICENSES files optional based on a cmake option Label PR based on Comment #6741: Issue comment #3181 (comment) created by Kha
September 20, 2024 13:49 2s
September 20, 2024 13:49 2s
fix: downgrade instance synth order issues to warnings Label PR based on Comment #6740: Issue comment #5399 (comment) created by Kha
September 20, 2024 13:48 2s
September 20, 2024 13:48 2s
exact? suggests term that does not work Label PR based on Comment #6739: Issue comment #5407 (comment) created by nomeata
September 20, 2024 13:36 4s
September 20, 2024 13:36 4s
feat: qsort with proven bounds and correctness proof Label PR based on Comment #6738: Issue comment #5346 (comment) created by lyphyser
September 20, 2024 13:32 3s
September 20, 2024 13:32 3s
RFC: lake: add command to fetch dependency sources Label PR based on Comment #6737: Issue comment #5342 (comment) created by nomeata
September 20, 2024 13:24 3s
September 20, 2024 13:24 3s
feat: manage nested inductive types in deriving Label PR based on Comment #6736: Issue comment #3160 (comment) created by nomeata
September 20, 2024 12:38 2s
September 20, 2024 12:38 2s
LLVM vs C backend performance Label PR based on Comment #6735: Issue comment #3192 (comment) created by hargoniX
September 20, 2024 12:21 2s
September 20, 2024 12:21 2s
compiler produces (kernel) function expected Label PR based on Comment #6734: Issue comment #1774 (comment) created by sgraf812
September 20, 2024 12:14 2s
September 20, 2024 12:14 2s
LLVM vs C backend performance Label PR based on Comment #6733: Issue comment #3192 (comment) created by Kha
September 20, 2024 12:06 2s
September 20, 2024 12:06 2s
Deprecate and remove inductive ... := Label PR based on Comment #6732: Issue comment #5236 (comment) created by digama0
September 20, 2024 12:04 3s
September 20, 2024 12:04 3s
chore: basic cleanups for bv_decide Label PR based on Comment #6731: Issue comment #5408 (comment) created by leanprover-community-mathlib4-bot
September 20, 2024 11:48 1s
September 20, 2024 11:48 1s
fix: modify projection instance binder info Label PR based on Comment #6730: Issue comment #5376 (comment) created by leanprover-community-bot
September 20, 2024 10:48 3s
September 20, 2024 10:48 3s
fix: downgrade instance synth order issues to warnings Label PR based on Comment #6729: Issue comment #5399 (comment) created by Kha
September 20, 2024 10:27 3s
September 20, 2024 10:27 3s