Skip to content

Actions: FrederickPu/pullback

Actions

All workflows

Actions

Loading...
Loading

Showing runs from all workflows
165 workflow runs
165 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
got rid of strucutural sorries and replaced with panic Lean Action CI #115: Commit 8732a11 pushed by FrederickPu
1m 50s main
main
1m 50s
added alignment constraints and simplified ctx Lean Action CI #114: Commit bce8f94 pushed by FrederickPu
1m 25s main
main
1m 25s
got rid of option monad and proved termination Lean Action CI #113: Commit b27062e pushed by FrederickPu
1m 26s main
main
1m 26s
switched oplus to ite Lean Action CI #112: Commit 46af583 pushed by FrederickPu
1m 55s main
main
1m 55s
sketched bidirectional interp function (does both values and types) Lean Action CI #111: Commit 4965df1 pushed by FrederickPu
1m 27s main
main
1m 27s
backup whnf stuff Lean Action CI #110: Commit bf7cceb pushed by FrederickPu
1m 34s main
main
1m 34s
got typelift deriving thing working Lean Action CI #109: Commit 208e34c pushed by FrederickPu
1m 36s main
main
1m 36s
got runction typelift instances working Lean Action CI #108: Commit 26ab0cd pushed by FrederickPu
1m 37s main
main
1m 37s
added TypeLift experiment Lean Action CI #107: Commit 333263c pushed by FrederickPu
1m 33s main
main
1m 33s
fixed hygien issue in mut_call Lean Action CI #106: Commit 60f65f8 pushed by FrederickPu
2m 31s main
main
2m 31s
added more tests Lean Action CI #105: Commit c2e9458 pushed by FrederickPu
1m 26s main
main
1m 26s
got dependent references working Lean Action CI #104: Commit 167bfc4 pushed by FrederickPu
1m 30s main
main
1m 30s
switch to space seperation for other let based mut_call syntax sugar Lean Action CI #103: Commit acd1637 pushed by FrederickPu
1m 28s main
main
1m 28s
made syntax a bit more ergonomic Lean Action CI #102: Commit 046aaf1 pushed by FrederickPu
1m 34s main
main
1m 34s
mutvars passing but no CPS form since it was pointless Lean Action CI #101: Commit 248b9d7 pushed by FrederickPu
1m 34s main
main
1m 34s
cps do with mutvars passed in to k Lean Action CI #100: Commit 8597f64 pushed by FrederickPu
1m 28s main
main
1m 28s
backup cps form do (no mutvar passing) Lean Action CI #99: Commit 6545875 pushed by FrederickPu
1m 39s main
main
1m 39s
changed contintuations to subtype for Lean Action CI #98: Commit bbe564c pushed by FrederickPu
1m 45s main
main
1m 45s
sketch proof except for loop and ifthenelse Lean Action CI #97: Commit aae154d pushed by FrederickPu
1m 55s main
main
1m 55s
added more necessary hypothesis to main theorem Lean Action CI #96: Commit 795b918 pushed by FrederickPu
2m 0s main
main
2m 0s
stated new correctness theorem for cps form eval and toSSAExpr! Lean Action CI #95: Commit f9381aa pushed by FrederickPu
1m 32s main
main
1m 32s
sketched CPS version SSADo.eval Lean Action CI #94: Commit 90ff47f pushed by FrederickPu
2m 1s main
main
2m 1s
added elimination rule theorems for new eval system Lean Action CI #93: Commit 87e0c9a pushed by FrederickPu
1m 24s main
main
1m 24s
switched to reduce based eval for expr Lean Action CI #92: Commit 27f750d pushed by FrederickPu
1m 28s main
main
1m 28s
split up ssaconst Lean Action CI #91: Commit 48b495f pushed by FrederickPu
1m 35s main
main
1m 35s