Skip to content

Actions: FrederickPu/pullback

Actions

All workflows

Actions

Loading...
Loading

Showing runs from all workflows
142 workflow runs
142 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
fixed logic in ifthenelse case Lean Action CI #142: Commit f43e204 pushed by FrederickPu
1m 31s main
main
1m 31s
proved inferType_ktype Lean Action CI #141: Commit 4989389 pushed by FrederickPu
1m 49s main
main
1m 49s
finished break and continue arms Lean Action CI #140: Commit 62afb5c pushed by FrederickPu
1m 28s main
main
1m 28s
fixed break and continue interp issues Lean Action CI #139: Commit 5a861b7 pushed by FrederickPu
1m 32s main
main
1m 32s
refactored continutation call sites to use mkmuttuple instead of dvector Lean Action CI #138: Commit 50ba26e pushed by FrederickPu
1m 39s main
main
1m 39s
grouped common have statment Lean Action CI #137: Commit 21be967 pushed by FrederickPu
1m 30s main
main
1m 30s
completed letM arm except for validVars Lean Action CI #136: Commit 47396d2 pushed by FrederickPu
2m 10s main
main
2m 10s
filled out more of letM arm Lean Action CI #135: Commit fc70b88 pushed by FrederickPu
1m 47s main
main
1m 47s
completed letE and sketched letM Lean Action CI #134: Commit 7507481 pushed by FrederickPu
1m 52s main
main
1m 52s
golfed down proof a bit Lean Action CI #133: Commit 194ef81 pushed by FrederickPu
1m 26s main
main
1m 26s
finished letE case for interp up to sorry about ktype roundtripping Lean Action CI #132: Commit 145dc3f pushed by FrederickPu
2m 10s main
main
2m 10s
added proof for continutation in letE Lean Action CI #131: Commit 5653b6a pushed by FrederickPu
1m 23s main
main
1m 23s
added useful lemmas and closed the expr case of interp Lean Action CI #130: Commit 7069735 pushed by FrederickPu
2m 58s main
main
2m 58s
initial sketch for SSADo.interp Lean Action CI #129: Commit a1e348d pushed by FrederickPu
1m 30s main
main
1m 30s
sketched front facing api for PDo and PExpr Lean Action CI #128: Commit 5d75ad9 pushed by FrederickPu
1m 29s main
main
1m 29s
switched to interp idea for explicit SSADo semantics Lean Action CI #127: Commit ac49221 pushed by FrederickPu
1m 30s main
main
1m 30s
sketched cps form eval idea Lean Action CI #126: Commit d6aa83c pushed by FrederickPu
1m 31s main
main
1m 31s
group conitutation hypothesis into predicate to make plumbing nicer Lean Action CI #125: Commit 419ad68 pushed by FrederickPu
1m 44s main
main
1m 44s
undid dumb dumb moment about seq and simplified plumbing Lean Action CI #124: Commit d74097f pushed by FrederickPu
4m 3s main
main
4m 3s
sketch loop proof for evalRefined Lean Action CI #123: Commit 1d12840 pushed by FrederickPu
1m 24s main
main
1m 24s
fixed kbreak logic in ifthenelse and improve evalRefined Lean Action CI #122: Commit 41c8bb5 pushed by FrederickPu
1m 57s main
main
1m 57s
extracted all sorries to external lemmas Lean Action CI #121: Commit c889df9 pushed by FrederickPu
1m 25s main
main
1m 25s
beefed up ctx alignment Lean Action CI #120: Commit 92b0415 pushed by FrederickPu
1m 29s main
main
1m 29s
made interp support non whnf and return alignment guarantee Lean Action CI #119: Commit 7eac821 pushed by FrederickPu
1m 30s main
main
1m 30s
explicit thread in WHNF constraint and only handle atomic applications Lean Action CI #118: Commit 4fac56e pushed by FrederickPu
1m 22s main
main
1m 22s