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
5,971 workflow runs
5,971 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

style: fix style in bv_decide normalizer Check for modules that should use `prelude` #5975: Pull request #5992 opened by hargoniX
November 7, 2024 11:38 1m 9s hbv/bv_decide_style
hbv/bv_decide_style
November 7, 2024 11:38 1m 9s
refactor: omega: avoid MVar machinery Check for modules that should use `prelude` #5974: Pull request #5991 opened by nomeata
November 7, 2024 11:29 13s joachim/omega-no-mvar
joachim/omega-no-mvar
November 7, 2024 11:29 13s
chore: fix test exclusion Check for modules that should use `prelude` #5973: Pull request #5990 opened by Kha
November 7, 2024 09:42 12s fix-
fix-
November 7, 2024 09:42 12s
feat: simp -underLambda Check for modules that should use `prelude` #5972: Pull request #5977 synchronize by nomeata
November 7, 2024 09:34 14s joachim/simp-underLambda
joachim/simp-underLambda
November 7, 2024 09:34 14s
feat: structure auto-completion & partial InfoTrees Check for modules that should use `prelude` #5971: Pull request #5835 synchronize by mhuisi
November 7, 2024 09:26 13s mhuisi:mhuisi/constructor-field-completion-2
mhuisi:mhuisi/constructor-field-completion-2
November 7, 2024 09:26 13s
feat: change Array.set to take a Nat and a tactic provided bound Check for modules that should use `prelude` #5970: Pull request #5988 synchronize by kim-em
November 7, 2024 08:58 16s change_array_Set
change_array_Set
November 7, 2024 08:58 16s
bisect step 1 Check for modules that should use `prelude` #5969: Pull request #5989 opened by Kha
November 7, 2024 08:53 13s Kha:bisect1
Kha:bisect1
November 7, 2024 08:53 13s
refactor: name the default SizeOf instance Check for modules that should use `prelude` #5968: Pull request #5981 synchronize by nomeata
November 7, 2024 08:51 14s joachim/instSizeOfDefault
joachim/instSizeOfDefault
November 7, 2024 08:51 14s
feat: structure auto-completion & partial InfoTrees Check for modules that should use `prelude` #5967: Pull request #5835 synchronize by Kha
November 7, 2024 08:44 12s mhuisi:mhuisi/constructor-field-completion-2
mhuisi:mhuisi/constructor-field-completion-2
November 7, 2024 08:44 12s
feat: change Array.set to take a Nat and a tactic provided bound Check for modules that should use `prelude` #5966: Pull request #5988 synchronize by kim-em
November 7, 2024 08:37 11s change_array_Set
change_array_Set
November 7, 2024 08:37 11s
feat: change Array.set to take a Nat and a tactic provided bound Check for modules that should use `prelude` #5965: Pull request #5988 opened by kim-em
November 7, 2024 08:35 12s change_array_Set
change_array_Set
November 7, 2024 08:35 12s
feat: simp local confluence testing Check for modules that should use `prelude` #5964: Pull request #5717 synchronize by kim-em
November 7, 2024 08:32 12s simplc
simplc
November 7, 2024 08:32 12s
feat: BitVec.getMsbD in bv_decide Check for modules that should use `prelude` #5963: Pull request #5987 opened by hargoniX
November 7, 2024 07:43 13s hbv/bv_decide_getMsbD
hbv/bv_decide_getMsbD
November 7, 2024 07:43 13s
feat: verify keys method on HashMaps Check for modules that should use `prelude` #5962: Pull request #5866 synchronize by TwoFX
November 7, 2024 07:13 12s monsterkrampe:hashmap-keys
monsterkrampe:hashmap-keys
November 7, 2024 07:13 12s
feat: simp local confluence testing Check for modules that should use `prelude` #5961: Pull request #5717 synchronize by kim-em
November 7, 2024 05:10 12s simplc
simplc
November 7, 2024 05:10 12s
chore: remove trivial from get_elem_tactic Check for modules that should use `prelude` #5960: Pull request #5986 synchronize by kim-em
November 7, 2024 05:01 12s rm_get_elem_tactic_trivial
rm_get_elem_tactic_trivial
November 7, 2024 05:01 12s
chore: remove trivial from get_elem_tactic Check for modules that should use `prelude` #5959: Pull request #5986 synchronize by kim-em
November 7, 2024 04:37 14s rm_get_elem_tactic_trivial
rm_get_elem_tactic_trivial
November 7, 2024 04:37 14s
chore: remove trivial from get_elem_tactic Check for modules that should use `prelude` #5958: Pull request #5986 opened by kim-em
November 7, 2024 04:36 11s rm_get_elem_tactic_trivial
rm_get_elem_tactic_trivial
November 7, 2024 04:36 11s
feat: lemmas relating Array.findX and List.findX Check for modules that should use `prelude` #5957: Pull request #5985 synchronize by kim-em
November 7, 2024 03:13 9s findSomeM
findSomeM
November 7, 2024 03:13 9s
feat: lemmas relating Array.findX and List.findX Check for modules that should use `prelude` #5956: Pull request #5985 opened by kim-em
November 7, 2024 03:12 10s findSomeM
findSomeM
November 7, 2024 03:12 10s
feat: interactions between List.foldX and List.filterX Check for modules that should use `prelude` #5955: Pull request #5984 opened by kim-em
November 7, 2024 02:14 1m 28s fold_filter
fold_filter
November 7, 2024 02:14 1m 28s
fix: out of scope let-variable can appear in fun binder type of metav… Check for modules that should use `prelude` #5954: Pull request #5948 synchronize by JovanGerb
November 7, 2024 01:32 11s JovanGerb:decl_has_free_variables
JovanGerb:decl_has_free_variables
November 7, 2024 01:32 11s
fix: out of scope let-variable can appear in fun binder type of metav… Check for modules that should use `prelude` #5953: Pull request #5948 synchronize by JovanGerb
November 6, 2024 23:22 13s JovanGerb:decl_has_free_variables
JovanGerb:decl_has_free_variables
November 6, 2024 23:22 13s
chore: upstream List.insertIdx from Batteries, lemmas from Mathlib, and revise lemmas Check for modules that should use `prelude` #5952: Pull request #5969 synchronize by kim-em
November 6, 2024 23:14 14s upstream_insertIdx
upstream_insertIdx
November 6, 2024 23:14 14s
feat: minor lemmas about List.ofFn Check for modules that should use `prelude` #5951: Pull request #5982 opened by kim-em
November 6, 2024 22:46 15s head_ofFn
head_ofFn
November 6, 2024 22:46 15s