Skip to content

Actions: leanprover/lean4

Actions

Check for modules that should use `prelude`

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
check-prelude.yml
1,006 workflow run results
1,006 workflow run results

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

chore: default for librarySearch tactic argument Check for modules that should use `prelude` #56: Pull request #3495 opened by kim-em
February 25, 2024 07:17 10s librarySearch_tactic_default
librarySearch_tactic_default
February 25, 2024 07:17 10s
fix: make Lean.Internal.liftCoeM and Lean.Internal.coeM unfold Check for modules that should use `prelude` #55: Pull request #3404 synchronize by kmill
February 25, 2024 06:15 11s kmill:lean_internal_coeM
kmill:lean_internal_coeM
February 25, 2024 06:15 11s
feat: syntax and delaborator for delayed assignment metavariables Check for modules that should use `prelude` #54: Pull request #3494 opened by kmill
February 25, 2024 06:02 19s kmill:pp_delayed_assignment
kmill:pp_delayed_assignment
February 25, 2024 06:02 19s
fix: match pattern literal support Check for modules that should use `prelude` #53: Pull request #3490 synchronize by leodemoura
February 24, 2024 23:27 10s match_lit_issues
match_lit_issues
February 24, 2024 23:27 10s
fix: make omission syntax a builtin syntax Check for modules that should use `prelude` #52: Pull request #3489 synchronize by kmill
February 24, 2024 19:17 15s kmill:omission_builtin
kmill:omission_builtin
February 24, 2024 19:17 15s
feat: add intMax Check for modules that should use `prelude` #51: Pull request #3492 opened by bollu
February 24, 2024 19:12 12s bollu:intmax
bollu:intmax
February 24, 2024 19:12 12s
fix: make omission syntax a builtin syntax Check for modules that should use `prelude` #50: Pull request #3489 synchronize by kmill
February 24, 2024 17:26 12s kmill:omission_builtin
kmill:omission_builtin
February 24, 2024 17:26 12s
fix: clean build after update-stage0 Check for modules that should use `prelude` #49: Pull request #3491 synchronize by Kha
February 24, 2024 15:17 13s Kha:fix-stage0
Kha:fix-stage0
February 24, 2024 15:17 13s
fix: clean build after update-stage0 Check for modules that should use `prelude` #48: Pull request #3491 opened by Kha
February 24, 2024 14:32 12s Kha:fix-stage0
Kha:fix-stage0
February 24, 2024 14:32 12s
feat: add lemmas about BitVec.concat and bitwise ops Check for modules that should use `prelude` #47: Pull request #3487 synchronize by alexkeizer
February 24, 2024 14:15 15s opencompl:concat-bitwise-ops
opencompl:concat-bitwise-ops
February 24, 2024 14:15 15s
fix: match pattern literal support Check for modules that should use `prelude` #46: Pull request #3490 synchronize by leodemoura
February 24, 2024 07:58 13s match_lit_issues
match_lit_issues
February 24, 2024 07:58 13s
fix: match pattern literal support Check for modules that should use `prelude` #45: Pull request #3490 opened by leodemoura
February 24, 2024 07:57 15s match_lit_issues
match_lit_issues
February 24, 2024 07:57 15s
fix: make omission syntax a builtin syntax Check for modules that should use `prelude` #44: Pull request #3489 opened by kmill
February 24, 2024 07:28 12s kmill:omission_builtin
kmill:omission_builtin
February 24, 2024 07:28 12s
fix: disable USize simprocs Check for modules that should use `prelude` #43: Pull request #3488 opened by leodemoura
February 24, 2024 02:24 13s no_usize_simproc
no_usize_simproc
February 24, 2024 02:24 13s
feat: add lemmas about BitVec.concat and bitwise ops Check for modules that should use `prelude` #42: Pull request #3487 opened by alexkeizer
February 24, 2024 02:05 11s opencompl:concat-bitwise-ops
opencompl:concat-bitwise-ops
February 24, 2024 02:05 11s
WIP: blast_bv tactic Check for modules that should use `prelude` #41: Pull request #3486 opened by alexkeizer
February 24, 2024 00:55 12s opencompl:bv-elim
opencompl:bv-elim
February 24, 2024 00:55 12s
perf: bitvector literals in match patterns Check for modules that should use `prelude` #40: Pull request #3485 opened by leodemoura
February 23, 2024 23:40 38s bv_lit_match_perf
bv_lit_match_perf
February 23, 2024 23:40 38s
fix: isDefEq handling of delayed-assigned mvars when withAssignableSyntheticOpaque is true Check for modules that should use `prelude` #39: Pull request #3473 synchronize by thorimur
February 23, 2024 23:02 13s thorimur:isDefEq-fvar-bug
thorimur:isDefEq-fvar-bug
February 23, 2024 23:02 13s
fix: isDefEq handling of delayed-assigned mvars when withAssignableSyntheticOpaque is true Check for modules that should use `prelude` #38: Pull request #3473 synchronize by thorimur
February 23, 2024 23:00 11s thorimur:isDefEq-fvar-bug
thorimur:isDefEq-fvar-bug
February 23, 2024 23:00 11s
fix: isDefEq handling of delayed-assigned mvars when withAssignableSyntheticOpaque is true Check for modules that should use `prelude` #37: Pull request #3473 synchronize by thorimur
February 23, 2024 22:48 38s thorimur:isDefEq-fvar-bug
thorimur:isDefEq-fvar-bug
February 23, 2024 22:48 38s
feat: ToExpr instances for Fin, BitVec, UInt8, ..., USize Check for modules that should use `prelude` #36: Pull request #3484 opened by leodemoura
February 23, 2024 22:38 15s toExprInsts
toExprInsts
February 23, 2024 22:38 15s
chore: move BitVec to top level namespace Check for modules that should use `prelude` #35: Pull request #3451 synchronize by leodemoura
February 23, 2024 22:30 12s bv_no_std
bv_no_std
February 23, 2024 22:30 12s
fix: isDefEq handling of delayed-assigned mvars when withAssignableSyntheticOpaque is true Check for modules that should use `prelude` #34: Pull request #3473 synchronize by thorimur
February 23, 2024 22:29 11s thorimur:isDefEq-fvar-bug
thorimur:isDefEq-fvar-bug
February 23, 2024 22:29 11s
fix: isDefEq handling of delayed-assigned mvars when withAssignableSyntheticOpaque is true Check for modules that should use `prelude` #33: Pull request #3473 synchronize by thorimur
February 23, 2024 22:20 12s thorimur:isDefEq-fvar-bug
thorimur:isDefEq-fvar-bug
February 23, 2024 22:20 12s
fix: isDefEq handling of delayed-assigned mvars when withAssignableSyntheticOpaque is true Check for modules that should use `prelude` #32: Pull request #3473 synchronize by thorimur
February 23, 2024 22:12 44s thorimur:isDefEq-fvar-bug
thorimur:isDefEq-fvar-bug
February 23, 2024 22:12 44s
ProTip! You can narrow down the results and go further in time using created:<2024-02-23 or the other filters available.