Skip to content

Actions: leanprover/lean4

Actions

Update stage0

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
update-stage0.yml
4,729 workflow runs
4,729 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

refactor: have telescope support (#11914) Update stage0 #6837: Commit c871f66 pushed by github-merge-queue bot
40s master
master
40s
doc: write a guideline for tactic docstrings (#11406) Update stage0 #6836: Commit 0f86623 pushed by github-merge-queue bot
38s master
master
38s
perf: replaceS and instantiateRevBetaS (#11911) Update stage0 #6835: Commit f6c8b8d pushed by github-merge-queue bot
38s master
master
38s
refactor: reorganize SymM and GrindM monad hierarchy (#11909) Update stage0 #6834: Commit 175661b pushed by github-merge-queue bot
38s master
master
38s
perf: add PersistentHashMap.findKeyD and PersistentHashSet.findD … Update stage0 #6833: Commit fd88637 pushed by github-merge-queue bot
40s master
master
40s
perf: use update.*! at AlphaShareCommon (#11906) Update stage0 #6832: Commit 7376772 pushed by github-merge-queue bot
39s master
master
39s
feat: add guards for grind patterns for getElem?_eq_none theorems (… Update stage0 #6831: Commit c358b0c pushed by github-merge-queue bot
40s master
master
40s
chore: cleanup grind List tests (#11903) Update stage0 #6830: Commit 8207919 pushed by github-merge-queue bot
38s master
master
38s
chore: cleanup some grind tests about palindromes (#11902) Update stage0 #6829: Commit 06b7b02 pushed by github-merge-queue bot
39s master
master
39s
fix: grind propagates 0 * a = 0 for CommSemiring (#11881) Update stage0 #6828: Commit 460b3c3 pushed by github-merge-queue bot
38s master
master
38s
feat: add Nat.gcd_left_comm and Int.gcd_left_comm (#11901) Update stage0 #6827: Commit b46688d pushed by github-merge-queue bot
38s master
master
38s
feat: pre and post may return "done" in Sym.simp (#11900) Update stage0 #6826: Commit 82f60a7 pushed by github-merge-queue bot
38s master
master
38s
chore: include comparator and lean4export in release process (#11899) Update stage0 #6825: Commit 6bf2486 pushed by github-merge-queue bot
39s master
master
39s
feat: simplify lambdas in Sym.simp (#11898) Update stage0 #6824: Commit f1c903c pushed by github-merge-queue bot
39s master
master
39s
fix: avoid panic in TagDeclarationExtension.tag on partial elaborat… Update stage0 #6823: Commit 35d8925 pushed by github-merge-queue bot
39s master
master
39s
chore: remove leftover (#11895) Update stage0 #6822: Commit 9f404d8 pushed by github-merge-queue bot
37s master
master
37s
perf: ensure withTraceNodeBefore message is created lazily (#11893) Update stage0 #6821: Commit 81c93ae pushed by github-merge-queue bot
41s master
master
41s
perf: optimize simp congruence proofs (#11892) Update stage0 #6820: Commit cf36ac9 pushed by github-merge-queue bot
32s master
master
32s
chore: include free variables (#11894) Update stage0 #6819: Commit 609d99e pushed by github-merge-queue bot
32s master
master
32s
feat: check Sym.simp thresholds (#11890) Update stage0 #6818: Commit 78c9a01 pushed by github-merge-queue bot
32s master
master
32s
perf: Sym.Simp.DiscrTree retrieval (#11889) Update stage0 #6817: Commit a2cf78a pushed by github-merge-queue bot
31s master
master
31s
refactor: Sym.simp (#11888) Update stage0 #6816: Commit bc72487 pushed by github-merge-queue bot
31s master
master
31s
feat: add discrimination tree retrieval for Sym (#11886) Update stage0 #6815: Commit b40dabd pushed by github-merge-queue bot
32s master
master
32s
feat: add insertPattern for discrimination tree insertion in Sym … Update stage0 #6814: Commit 19df2c4 pushed by github-merge-queue bot
32s master
master
32s
chore: fix typo (#11883) Update stage0 #6813: Commit ce8fdb1 pushed by github-merge-queue bot
32s master
master
32s