Skip to content

Actions: leanprover/lean4

Actions

Check awaiting-mathlib label

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
awaiting-mathlib.yml
10,964 workflow run results
10,964 workflow run results

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

chore: remove NullCert leftovers Check awaiting-mathlib label #10963: Pull request #9955 labeled by leodemoura
5s grind_null_leftovers
grind_null_leftovers
5s
chore: remove NullCert leftovers Check awaiting-mathlib label #10964: Pull request #9955 opened by leodemoura
9s grind_null_leftovers
grind_null_leftovers
9s
feat: make intros x y z be intro x y z; intros Check awaiting-mathlib label #10961: Pull request #9943 unlabeled by leanprover-community-bot
4s kmill:kmill_intros_macro
kmill:kmill_intros_macro
4s
feat: make intros x y z be intro x y z; intros Check awaiting-mathlib label #10962: Pull request #9943 labeled by leanprover-community-bot
5s kmill:kmill_intros_macro
kmill:kmill_intros_macro
5s
Check awaiting-mathlib label Check awaiting-mathlib label #10960: Merge group checks requested
8s
8s
Check awaiting-mathlib label Check awaiting-mathlib label #10959: Merge group checks requested
8s
8s
Check awaiting-mathlib label Check awaiting-mathlib label #10958: Merge group checks requested
9s
9s
chore: remove grind +ringNull option Check awaiting-mathlib label #10957: Pull request #9954 synchronize by leodemoura
8s grind_no_null
grind_no_null
8s
chore: remove grind +ringNull option Check awaiting-mathlib label #10955: Pull request #9954 opened by leodemoura
5s grind_no_null
grind_no_null
5s
chore: remove grind +ringNull option Check awaiting-mathlib label #10956: Pull request #9954 labeled by leodemoura
5s grind_no_null
grind_no_null
5s
feat: make intros x y z be intro x y z; intros Check awaiting-mathlib label #10954: Pull request #9943 synchronize by kmill
5s kmill:kmill_intros_macro
kmill:kmill_intros_macro
5s
feat: T.ctor.elim single-constructor cases function Check awaiting-mathlib label #10952: Pull request #9952 opened by nomeata
8s joachim/withCtor
joachim/withCtor
8s
feat: T.ctor.elim single-constructor cases function Check awaiting-mathlib label #10953: Pull request #9952 labeled by nomeata
6s joachim/withCtor
joachim/withCtor
6s
feat: clean up type annotations when elaborating declaration bodies Check awaiting-mathlib label #10951: Pull request #9674 labeled by leanprover-bot
4s kmill:kmill_cleanup_lctx
kmill:kmill_cleanup_lctx
4s
feat: make intros x y z be intro x y z; intros Check awaiting-mathlib label #10950: Pull request #9943 synchronize by kmill
8s kmill:kmill_intros_macro
kmill:kmill_intros_macro
8s
feat: tactic info per intro hypothesis, rfl pattern Check awaiting-mathlib label #10949: Pull request #9942 synchronize by kmill
5s kmill:kmill_intro_steps
kmill:kmill_intro_steps
5s
feat: clean up type annotations when elaborating declaration bodies Check awaiting-mathlib label #10948: Pull request #9674 synchronize by kmill
9s kmill:kmill_cleanup_lctx
kmill:kmill_cleanup_lctx
9s
feat: .ctorIdx for all inductives Check awaiting-mathlib label #10947: Pull request #9951 synchronize by nomeata
6s joachim/ctorIdx
joachim/ctorIdx
6s
feat: .ctorIdx for all inductives Check awaiting-mathlib label #10946: Pull request #9951 labeled by leanprover-community-bot
5s joachim/ctorIdx
joachim/ctorIdx
5s
fix: local syntax should create private definitions Check awaiting-mathlib label #10945: Pull request #9915 synchronize by Kha
6s Kha:push-mszkszvxwolz
Kha:push-mszkszvxwolz
6s
feat: tactic info per intro hypothesis, rfl pattern Check awaiting-mathlib label #10944: Pull request #9942 synchronize by kmill
6s kmill:kmill_intro_steps
kmill:kmill_intro_steps
6s
feat: .ctorIdx for all inductives Check awaiting-mathlib label #10943: Pull request #9951 labeled by leanprover-bot
7s joachim/ctorIdx
joachim/ctorIdx
7s
feat: tactic info per intro hypothesis, rfl pattern Check awaiting-mathlib label #10942: Pull request #9942 synchronize by kmill
10s kmill:kmill_intro_steps
kmill:kmill_intro_steps
10s
feat: tactic info per intro hypothesis, rfl pattern Check awaiting-mathlib label #10941: Pull request #9942 synchronize by kmill
7s kmill:kmill_intro_steps
kmill:kmill_intro_steps
7s
experiment: definitional well-founded recursion Check awaiting-mathlib label #10940: Pull request #9944 synchronize by cppio
9s cppio:wf-defeq
cppio:wf-defeq
9s