Skip to content

Actions: leanprover/lean4

Actions

Check for copyright header

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
copyright-header.yml
10,972 workflow run results
10,972 workflow run results

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

chore: remove NullCert leftovers Check for copyright header #16652: Pull request #9955 opened by leodemoura
44s grind_null_leftovers
grind_null_leftovers
44s
chore: remove grind +ringNull option Check for copyright header #16651: Pull request #9954 synchronize by leodemoura
24s grind_no_null
grind_no_null
24s
chore: remove grind +ringNull option Check for copyright header #16650: Pull request #9954 opened by leodemoura
26s grind_no_null
grind_no_null
26s
feat: make intros x y z be intro x y z; intros Check for copyright header #16649: Pull request #9943 synchronize by kmill
26s kmill:kmill_intros_macro
kmill:kmill_intros_macro
26s
feat: T.ctor.elim single-constructor cases function Check for copyright header #16648: Pull request #9952 opened by nomeata
24s joachim/withCtor
joachim/withCtor
24s
feat: make intros x y z be intro x y z; intros Check for copyright header #16647: Pull request #9943 synchronize by kmill
28s kmill:kmill_intros_macro
kmill:kmill_intros_macro
28s
feat: tactic info per intro hypothesis, rfl pattern Check for copyright header #16646: Pull request #9942 synchronize by kmill
26s kmill:kmill_intro_steps
kmill:kmill_intro_steps
26s
feat: clean up type annotations when elaborating declaration bodies Check for copyright header #16645: Pull request #9674 synchronize by kmill
27s kmill:kmill_cleanup_lctx
kmill:kmill_cleanup_lctx
27s
feat: .ctorIdx for all inductives Check for copyright header #16644: Pull request #9951 synchronize by nomeata
28s joachim/ctorIdx
joachim/ctorIdx
28s
fix: local syntax should create private definitions Check for copyright header #16643: Pull request #9915 synchronize by Kha
28s Kha:push-mszkszvxwolz
Kha:push-mszkszvxwolz
28s
feat: tactic info per intro hypothesis, rfl pattern Check for copyright header #16642: Pull request #9942 synchronize by kmill
26s kmill:kmill_intro_steps
kmill:kmill_intro_steps
26s
feat: tactic info per intro hypothesis, rfl pattern Check for copyright header #16641: Pull request #9942 synchronize by kmill
27s kmill:kmill_intro_steps
kmill:kmill_intro_steps
27s
feat: tactic info per intro hypothesis, rfl pattern Check for copyright header #16640: Pull request #9942 synchronize by kmill
25s kmill:kmill_intro_steps
kmill:kmill_intro_steps
25s
experiment: definitional well-founded recursion Check for copyright header #16639: Pull request #9944 synchronize by cppio
28s cppio:wf-defeq
cppio:wf-defeq
28s
feat: .ctorIdx for all inductives Check for copyright header #16638: Pull request #9951 opened by nomeata
25s joachim/ctorIdx
joachim/ctorIdx
25s
perf: deduplicate core computation inside mkCongrSimpForConst? Check for copyright header #16637: Pull request #9300 synchronize by Kha
25s Kha:push-nzlortxnlrwo
Kha:push-nzlortxnlrwo
25s
feat: tree map lemmas for filter, map, filterMap Check for copyright header #16636: Pull request #9632 synchronize by Rob23oba
25s Rob23oba:treemap-filter-map
Rob23oba:treemap-filter-map
25s
chore: fix failing mk*Sorry in bootstrapping contexts Check for copyright header #16635: Pull request #9950 opened by Kha
23s Kha:push-lxtnnylkunxl
Kha:push-lxtnnylkunxl
23s
perf: deduplicate core computation inside mkCongrSimpForConst? Check for copyright header #16633: Pull request #9300 synchronize by Kha
22s Kha:push-nzlortxnlrwo
Kha:push-nzlortxnlrwo
22s
fix: local syntax should create private definitions Check for copyright header #16634: Pull request #9915 synchronize by Kha
26s Kha:push-mszkszvxwolz
Kha:push-mszkszvxwolz
26s
perf: make inj/injEq realizable constants Check for copyright header #16632: Pull request #9934 synchronize by Kha
24s Kha:push-yumtuqwyxwlz
Kha:push-yumtuqwyxwlz
24s
perf: deduplicate core computation inside mkCongrSimpForConst? Check for copyright header #16631: Pull request #9300 synchronize by Kha
24s Kha:push-nzlortxnlrwo
Kha:push-nzlortxnlrwo
24s
fix: remove dependency on LawfulBEq from List.lookup lemmas Check for copyright header #16630: Pull request #9949 opened by tom93
23s tom93:pr/fix-list-lookup-lawfulbeq
tom93:pr/fix-list-lookup-lawfulbeq
23s
perf: try to reduce amount of code generated by HashMaps Check for copyright header #16629: Pull request #9941 synchronize by Kha
24s hbv/hashmap_less_inline
hbv/hashmap_less_inline
24s
feat: trim grind linarith proof context Check for copyright header #16628: Pull request #9947 opened by leodemoura
23s grind_linarith_trim_proof
grind_linarith_trim_proof
23s