Skip to content

Actions: m4lvin/lean4-pdl

Actions

CI

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
build.yml
683 workflow runs
683 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

prove PathIn.nil_eq_append_iff_both_eq_nil CI #616: Commit ccba79f pushed by m4lvin
July 29, 2024 11:56 4m 39s main
main
July 29, 2024 11:56 4m 39s
tableauThenNotSat: reduce non-loaded case to lemmas about append nil CI #615: Commit 3a77b60 pushed by m4lvin
July 28, 2024 21:14 4m 42s main
main
July 28, 2024 21:14 4m 42s
tableauThenNotSat: loaded case almost done CI #614: Commit 6460ebf pushed by m4lvin
July 28, 2024 15:58 4m 44s main
main
July 28, 2024 15:58 4m 44s
two separate IHs in tableautheNotSat + foldr boxes CI #613: Commit afed278 pushed by m4lvin
July 28, 2024 14:33 4m 45s main
main
July 28, 2024 14:33 4m 45s
working on loadedDiamondPaths + some reorganizing CI #612: Commit 51f87b0 pushed by m4lvin
July 27, 2024 21:11 4m 29s main
main
July 27, 2024 21:11 4m 29s
Expand SemQuot example a bit CI #611: Commit d832bee pushed by goens
July 25, 2024 12:21 4m 34s quots
quots
July 25, 2024 12:21 4m 34s
experiment with edge via seven cases and edgeCases CI #610: Commit a09ca2e pushed by m4lvin
July 23, 2024 09:48 4m 35s edge-seven-cases
edge-seven-cases
July 23, 2024 09:48 4m 35s
separate UnfoldBox and UnfoldDia CI #609: Commit 2c6d8f6 pushed by m4lvin
July 22, 2024 16:39 5m 0s main
main
July 22, 2024 16:39 5m 0s
idea to define the semEquiv Quotient CI #608: Commit 9d6710f pushed by m4lvin
July 22, 2024 16:25 5m 9s main
main
July 22, 2024 16:25 5m 9s
ideas for three alternative edge definitions CI #607: Commit 453e9ca pushed by m4lvin
July 14, 2024 10:26 5m 11s main
main
July 14, 2024 10:26 5m 11s
some pieces for localInterpolantStep CI #606: Commit 6cea52b pushed by m4lvin
July 11, 2024 20:22 5m 6s main
main
July 11, 2024 20:22 5m 6s
prove eProp2.e CI #605: Commit 2719c88 pushed by m4lvin
July 11, 2024 18:38 5m 15s main
main
July 11, 2024 18:38 5m 15s
resolving the use of O_def CI #604: Commit 0422259 pushed by m4lvin
July 10, 2024 21:59 4m 55s main
main
July 10, 2024 21:59 4m 55s
rename ClosedTableau to Tableau CI #603: Commit c7ee6db pushed by m4lvin
July 10, 2024 21:03 4m 59s main
main
July 10, 2024 21:03 4m 59s
adjust rewind, some ideas for eProp2.c, all comp and rep are loaded CI #602: Commit 9856db5 pushed by m4lvin
July 10, 2024 19:50 5m 11s main
main
July 10, 2024 19:50 5m 11s
repair and shorten stuff, but some still broken CI #601: Commit acbeeb0 pushed by m4lvin
July 9, 2024 21:10 5m 6s simplerF
simplerF
July 9, 2024 21:10 5m 6s
work on eProp2.c CI #600: Commit b64f5b7 pushed by m4lvin
July 9, 2024 21:06 5m 9s main
main
July 9, 2024 21:06 5m 9s
work on eProp2.c CI #599: Commit b64f5b7 pushed by m4lvin
July 9, 2024 21:05 5m 18s companion
companion
July 9, 2024 21:05 5m 18s
prove eProp2.f CI #598: Commit 31420fc pushed by m4lvin
July 8, 2024 21:29 5m 5s companion
companion
July 8, 2024 21:29 5m 5s
some progress in tableauThenNotSat CI #597: Commit 3eb8dd0 pushed by m4lvin
July 8, 2024 16:45 5m 29s companion
companion
July 8, 2024 16:45 5m 29s
fix loadL and loadR rule CI #596: Commit 3b86ccf pushed by m4lvin
July 7, 2024 20:54 4m 57s companion
companion
July 7, 2024 20:54 4m 57s
redefine LoadFormula with mutual AnyFormula CI #595: Commit 75644ea pushed by m4lvin
July 7, 2024 20:45 4m 56s companion
companion
July 7, 2024 20:45 4m 56s
more soundness; move endOf and child helper functions CI #594: Commit dbdcf22 pushed by m4lvin
July 7, 2024 18:54 5m 8s companion
companion
July 7, 2024 18:54 5m 8s
work on eProp2 and tableauThenNotSat, redefine nodeAt via tabAt CI #593: Commit 62b0351 pushed by m4lvin
July 7, 2024 14:17 4m 54s companion
companion
July 7, 2024 14:17 4m 54s
repair and shorten stuff, but some still broken CI #592: Commit d8a9bf5 pushed by m4lvin
July 6, 2024 16:37 4m 43s simplerF
simplerF
July 6, 2024 16:37 4m 43s