Skip to content

Actions: objectionary/proof

Actions

Lean (build)

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
lean.yml
208 workflow runs
208 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

Add comments and group mapAttrList properties Lean (build) #58: Commit a13b174 pushed by eyihluyc
February 1, 2024 22:26 50s substitution-lemma
substitution-lemma
February 1, 2024 22:26 50s
Add assumption about min free loc Lean (build) #57: Commit 0befa1c pushed by eyihluyc
February 1, 2024 21:35 45s substitution-lemma
substitution-lemma
February 1, 2024 21:35 45s
Confluence of parallel reduce Lean (build) #56: Pull request #17 opened by Anatolay
February 1, 2024 12:15 1m 48s confluence
confluence
February 1, 2024 12:15 1m 48s
Add subst_inc_cancel Lean (build) #55: Commit 5c58755 pushed by eyihluyc
February 1, 2024 05:33 44s substitution-lemma
substitution-lemma
February 1, 2024 05:33 44s
Fix sorry in preduce_incLocatorsFrom Lean (build) #54: Commit def10f8 pushed by eyihluyc
January 31, 2024 00:01 41s substitution-lemma
substitution-lemma
January 31, 2024 00:01 41s
Prove that confluence follows from local confluence (diamond property) Lean (build) #53: Commit 578cd06 pushed by Anatolay
January 30, 2024 16:41 1m 47s confluence
confluence
January 30, 2024 16:41 1m 47s
Add pcongOBJ case to preduce_incLocatorsFrom Lean (build) #52: Commit d27eb99 pushed by Anatolay
January 30, 2024 15:23 49s substitution-lemma
substitution-lemma
January 30, 2024 15:23 49s
Add substitution lemma and necessary definitions Lean (build) #51: Commit 2ba81ba pushed by eyihluyc
January 30, 2024 05:30 51s substitution-lemma
substitution-lemma
January 30, 2024 05:30 51s
[WIP] Add proof that confluence follows from strong confluence (diamo… Lean (build) #50: Commit 1ca0a17 pushed by Anatolay
January 29, 2024 14:50 2m 5s confluence
confluence
January 29, 2024 14:50 2m 5s
Add several cases to Proposition 3.8 (Half diamond) Lean (build) #49: Commit c9f5295 pushed by Anatolay
January 29, 2024 11:40 1m 42s confluence
confluence
January 29, 2024 11:40 1m 42s
Add lemmas A8 and A9 Lean (build) #48: Commit c35c494 pushed by eyihluyc
January 26, 2024 06:11 1m 41s substitution-lemma
substitution-lemma
January 26, 2024 06:11 1m 41s
Add definition of complete development Lean (build) #47: Commit 5bb8392 pushed by eyihluyc
January 25, 2024 23:40 36s confluence
confluence
January 25, 2024 23:40 36s
Add WIP for subst_swap Lean (build) #46: Commit a712480 pushed by eyihluyc
January 25, 2024 23:40 36s confluence
confluence
January 25, 2024 23:40 36s
[WIP] Add proof of substitution lemma Lean (build) #45: Commit c13cfd8 pushed by Anatolay
January 25, 2024 12:05 1m 47s substitution
substitution
January 25, 2024 12:05 1m 47s
Add WIP for subst_swap Lean (build) #44: Commit a712480 pushed by eyihluyc
January 24, 2024 21:19 48s substitution-lemma
substitution-lemma
January 24, 2024 21:19 48s
Merge pull request #11 from objectionary/equivalence-of-closures Lean (build) #43: Commit 0111929 pushed by eyihluyc
January 24, 2024 21:05 1m 48s substitution-lemma
substitution-lemma
January 24, 2024 21:05 1m 48s
Merge pull request #11 from objectionary/equivalence-of-closures Lean (build) #42: Commit 0111929 pushed by fizruk
January 24, 2024 18:39 1m 51s master
master
January 24, 2024 18:39 1m 51s
Add proofs of equivalence of closures of regular and parallel reductions Lean (build) #41: Pull request #11 opened by eyihluyc
January 24, 2024 15:33 1m 55s equivalence-of-closures
equivalence-of-closures
January 24, 2024 15:33 1m 55s
Refactor proofs of cong of redmany Lean (build) #40: Commit bc6ec7a pushed by eyihluyc
January 24, 2024 15:23 1m 41s equivalence-of-closures
equivalence-of-closures
January 24, 2024 15:23 1m 41s
Merge pull request #10 from objectionary/unique-attributes Lean (build) #39: Commit 017a426 pushed by Anatolay
January 23, 2024 13:16 1m 53s master
master
January 23, 2024 13:16 1m 53s
Add regular and parallel reductions and transitions between them Lean (build) #38: Pull request #10 opened by Anatolay
January 23, 2024 12:04 1m 41s unique-attributes
unique-attributes
January 23, 2024 12:04 1m 41s
Add missing definitions Lean (build) #37: Commit 900ec60 pushed by Anatolay
January 23, 2024 09:13 1m 49s unique-attributes
unique-attributes
January 23, 2024 09:13 1m 49s
Add pcongOBJ case in par_to_redMany Lean (build) #36: Commit fac9c8a pushed by eyihluyc
January 23, 2024 03:00 1m 48s unique-attributes
unique-attributes
January 23, 2024 03:00 1m 48s
Remove dead code Lean (build) #35: Commit 6884f74 pushed by Anatolay
January 22, 2024 13:56 30s unique-attributes
unique-attributes
January 22, 2024 13:56 30s
Make data carry uniqueness proof, refactor datatypes Lean (build) #34: Commit 54e437e pushed by Anatolay
January 18, 2024 19:19 47s unique-attributes
unique-attributes
January 18, 2024 19:19 47s