Skip to content

Actions: focs-lab/trace-theory-lean

Actions

Lean Action CI

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
lean_action_ci.yml
214 workflow runs
214 workflow runs

Filter by Event

⌥ + click/return to exclude

Filter by Status

⌥ + click/return to exclude

Filter by Branch

⌥ + click/return to exclude

Filter by Actor

⌥ + click/return to exclude
Improve lemmas Lean Action CI #139: Commit d2084c0 pushed by jefrai
2m 10s jeff-working
jeff-working
2m 10s
Add Ochmanski Theorem 4.1 (iii) => (iv) Lean Action CI #138: Commit 747073f pushed by jefrai
2m 25s jeff-working
jeff-working
2m 25s
Fix partial Theorem 4.1 (iii) => (iv) Lean Action CI #137: Commit 3a32dee pushed by jefrai
2m 18s jeff-working
jeff-working
2m 18s
Fix connectedness definition Lean Action CI #136: Commit 729f051 pushed by jefrai
2m 38s jeff-working
jeff-working
2m 38s
Add Ochmanski Theorem 4.1 (ii) => (iii) Lean Action CI #135: Commit f11951f pushed by jefrai
2m 23s jeff-working
jeff-working
2m 23s
Add lemma that interpreting a RatExp on Trace languages = interpretin… Lean Action CI #134: Commit 2c7a3cd pushed by jefrai
3m 12s jeff-working
jeff-working
3m 12s
Computability.lean: Update to match mathlib PR version Lean Action CI #133: Commit 3b014cd pushed by yisiox
4m 37s ys-working
ys-working
4m 37s
Add Prop 4.1 :: (i) <-> (iv) Lean Action CI #132: Commit 4f788ca pushed by jefrai
5s jeff-working
jeff-working
5s
Refine proof of correctness of toRegex further Lean Action CI #131: Commit 806a54c pushed by yisiox
4s ys-working
ys-working
4s
Refine IsRestrictedPath proofs Lean Action CI #130: Commit 416a7d2 pushed by yisiox
4s ys-working
ys-working
4s
Improve Kleene's Theorem by cleaning up and removing Classical Lean Action CI #129: Commit d41a6e5 pushed by yisiox
5s ys-working
ys-working
5s
Complete proof of Kleene's theorem epsilon NFA to regex direction Lean Action CI #128: Commit ac4de22 pushed by yisiox
5s ys-working
ys-working
5s
Progress proof of every regular language has a regular expression mat… Lean Action CI #127: Commit 96ad93a pushed by yisiox
5s ys-working
ys-working
5s
Fix variable naming of isRestrictedPath_iff_isPath Lean Action CI #126: Commit 5aae34e pushed by yisiox
6s ys-working
ys-working
6s
Add matches'_foldl_sum helper and progress Kleene's theorem Lean Action CI #125: Commit d153f47 pushed by yisiox
4s ys-working
ys-working
4s
Update attempt of Kleene's theorem via Kleene's algorithm Lean Action CI #124: Commit 294432b pushed by yisiox
6s ys-working
ys-working
6s
Add decidability tags to DFA and NFA constructions Lean Action CI #123: Commit dfc6cea pushed by yisiox
5s ys-working
ys-working
5s
Patch Prop 4.1 :: (i) -> (ii) hole Lean Action CI #122: Commit 27b9289 pushed by jefrai
5s jeff-working
jeff-working
5s
Sketch Prop 4.1 :: (i) -> (ii) Lean Action CI #121: Commit 08854cc pushed by jefrai
5s jeff-working
jeff-working
5s
Add comments to function definitions in Computability.lean Lean Action CI #120: Commit b32e9e1 pushed by yisiox
4s ys-working
ys-working
4s
Clean up DFA section Lean Action CI #119: Commit ffad2e0 pushed by yisiox
4s ys-working
ys-working
4s
Add first direction of Kleene's theorem Lean Action CI #118: Commit 8e9741e pushed by yisiox
4s ys-working
ys-working
4s
Complete proof that regular languages are closed under Kleene star Lean Action CI #117: Commit 8ad59b7 pushed by yisiox
4s ys-working
ys-working
4s
Rename helper lemma for closure under Kleene star Lean Action CI #116: Commit 4a7b922 pushed by yisiox
4s ys-working
ys-working
4s
Update concat and kstar lemmas Lean Action CI #115: Commit 2462682 pushed by yisiox
4s ys-working
ys-working
4s