Skip to content

Actions: WegmannDavid/LambdaLab

Actions

All workflows

Actions

Loading...
Loading

Showing runs from all workflows
118 workflow runs
118 workflow runs

Filter by Workflow

⌥ + click/return to exclude

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
Validate the seven motives, and correct my estimate of what is left Lean Action CI #118: Commit 1599f88 pushed by WegmannDavid
2m 14s parser-experimentation
parser-experimentation
2m 14s
Prove where the greedy folds stop -- the last prerequisite Lean Action CI #117: Commit 9af6fd7 pushed by WegmannDavid
1m 42s parser-experimentation
parser-experimentation
1m 42s
Decompose the two left-recursive chains -- the fold blocker Lean Action CI #116: Commit c7fe5b6 pushed by WegmannDavid
3m 55s parser-experimentation
parser-experimentation
3m 55s
Prove operator bodies are seamed, the second prerequisite Lean Action CI #115: Commit 7b45b58 pushed by WegmannDavid
1m 37s parser-experimentation
parser-experimentation
1m 37s
Prove the per-level seam lemma parseExpr_exact needs Lean Action CI #114: Commit 2845d9d pushed by WegmannDavid
2m 5s parser-experimentation
parser-experimentation
2m 5s
Clear every non-sorry build warning Lean Action CI #113: Commit efcb30f pushed by WegmannDavid
1m 58s parser-experimentation
parser-experimentation
1m 58s
Say so when the file suffix disagrees with the compiler Lean Action CI #112: Commit b6eb822 pushed by WegmannDavid
1m 29s parser-experimentation
parser-experimentation
1m 29s
Accept directories, and stop crashing on one Lean Action CI #111: Commit f99eef6 pushed by WegmannDavid
1m 53s parser-experimentation
parser-experimentation
1m 53s
Replace the playground with one compiler per language Lean Action CI #110: Commit 8ef30a5 pushed by WegmannDavid
1m 28s parser-experimentation
parser-experimentation
1m 28s
Split Pipeline into stages and one file that chains them Lean Action CI #109: Commit 48ad769 pushed by WegmannDavid
2m 15s parser-experimentation
parser-experimentation
2m 15s
Ignore .vscode/, as /.claude/ already is Lean Action CI #108: Commit 5932b6c pushed by WegmannDavid
1m 52s parser-experimentation
parser-experimentation
1m 52s
Demonstrate cross-declaration inference in the stlc example Lean Action CI #107: Commit 5aaac31 pushed by WegmannDavid
1m 45s parser-experimentation
parser-experimentation
1m 45s
Move Elaboratable's fields to the classes that own them Lean Action CI #106: Commit 70f2821 pushed by WegmannDavid
2m 3s parser-experimentation
parser-experimentation
2m 3s
Derive the program elaborator from the object language's Lean Action CI #105: Commit 50b9e50 pushed by WegmannDavid
1m 55s parser-experimentation
parser-experimentation
1m 55s
Prove GenerationComplete Lean Action CI #104: Commit fac0e11 pushed by WegmannDavid
1m 45s parser-experimentation
parser-experimentation
1m 45s
LawfulMVars extends both parents, closing the TypeSystem diamond Lean Action CI #103: Commit 9d932ee pushed by WegmannDavid
2m 4s parser-experimentation
parser-experimentation
2m 4s
LawfulMVars: typing is stable under substitution Lean Action CI #102: Commit cc899d7 pushed by WegmannDavid
1m 28s parser-experimentation
parser-experimentation
1m 28s
Target.elaborate: drop the vestigial Γ.Ground condition Lean Action CI #101: Commit 576b526 pushed by WegmannDavid
1m 28s parser-experimentation
parser-experimentation
1m 28s
Move MGUProp to Substitution/Unification/MGU.lean, and inhabit it Lean Action CI #100: Commit 0a553a2 pushed by WegmannDavid
1m 40s parser-experimentation
parser-experimentation
1m 40s
Stlc/Named/TypeSystem.lean: STLC against the TypeSystem classes Lean Action CI #99: Commit 735d1e6 pushed by WegmannDavid
1m 58s parser-experimentation
parser-experimentation
1m 58s
Stlc/Named/TypedLanguage.lean: STLC as a TypeSystem Lean Action CI #98: Commit 6852f17 pushed by WegmannDavid
1m 48s parser-experimentation
parser-experimentation
1m 48s
Name every plug-in file Pipeline.lean Lean Action CI #97: Commit 6ccade4 pushed by WegmannDavid
2m 15s parser-experimentation
parser-experimentation
2m 15s
TypedLanguage.Basic: make TypeSystem compile, and put it in the root Lean Action CI #96: Commit 69ac712 pushed by WegmannDavid
1m 44s parser-experimentation
parser-experimentation
1m 44s
Split the LambdaLab.Language namespace to match the new folders Lean Action CI #95: Commit 485e68e pushed by WegmannDavid
2m 21s parser-experimentation
parser-experimentation
2m 21s
Reorganize: Language/ -> Pipeline/, and TypedLanguage/ for the name l… Lean Action CI #94: Commit bccd79e pushed by WegmannDavid
1m 53s parser-experimentation
parser-experimentation
1m 53s