Skip to content

Actions: m4lvin/lean4-pdl

Actions

All workflows

Actions

Loading...
Loading

Showing runs from all workflows
740 workflow runs
740 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

localRuleApp.decreases_DM via List.Subperm.append
CI #670: Commit 7035cba pushed by m4lvin
September 30, 2024 22:01 4m 36s subperm
September 30, 2024 22:01 4m 36s
working on unfoldBoxContent
CI #669: Commit d308c26 pushed by m4lvin
September 30, 2024 20:33 4m 26s main
September 30, 2024 20:33 4m 26s
[main]: prove boxHelperTermination
Codespaces Prebuilds #53: by github-codespaces bot
September 30, 2024 06:00 17m 29s
September 30, 2024 06:00 17m 29s
prove boxHelperTermination
CI #668: Commit bd9d185 pushed by m4lvin
September 29, 2024 20:11 4m 48s main
September 29, 2024 20:11 4m 48s
finish LocalRule.Decreases and work on related parts
CI #667: Commit 3690305 pushed by m4lvin
September 25, 2024 19:32 4m 19s main
September 25, 2024 19:32 4m 19s
prove unfoldBox.decreases_lmOf_nonAtomic
CI #666: Commit 9cd07b5 pushed by m4lvin
September 25, 2024 06:52 4m 18s main
September 25, 2024 06:52 4m 18s
tweak lmOf measure; dia/box only non-atomic; unfoldBoxContent
CI #665: Commit f6329b8 pushed by m4lvin
September 24, 2024 21:07 4m 6s main
September 24, 2024 21:07 4m 6s
tweak lmOf measure; dia/box only non-atomic; unfoldBoxContent
CI #664: Commit f6329b8 pushed by m4lvin
September 24, 2024 21:07 4m 23s fixing_ldp
September 24, 2024 21:07 4m 23s
freeL and freeR cases in loadedDiamondPaths
CI #663: Commit 0048658 pushed by m4lvin
September 23, 2024 20:39 4m 15s fixing_ldp
September 23, 2024 20:39 4m 15s
tableauThenNotSat is sorry-free again
CI #662: Commit a378555 pushed by m4lvin
September 23, 2024 20:34 4m 16s fixing_ldp
September 23, 2024 20:34 4m 16s
ldp is still too weak
CI #661: Commit b88cbc8 pushed by m4lvin
September 23, 2024 18:47 4m 21s fixing_ldp
September 23, 2024 18:47 4m 21s
change statement and use of loadedDiamondPaths
CI #660: Commit b6537fe pushed by m4lvin
September 23, 2024 17:02 4m 28s fixing_ldp
September 23, 2024 17:02 4m 28s
[main]: ideas and thoughts in loadedDiamondPaths proof
Codespaces Prebuilds #52: by github-codespaces bot
September 23, 2024 06:00 16m 15s
September 23, 2024 06:00 16m 15s
ideas and thoughts in loadedDiamondPaths proof
CI #659: Commit 58215c0 pushed by m4lvin
September 22, 2024 13:11 4m 10s main
September 22, 2024 13:11 4m 10s
thinking about loadedDiamondPaths - need a local version too?
CI #658: Commit 6297b8e pushed by m4lvin
September 21, 2024 16:51 4m 21s main
September 21, 2024 16:51 4m 21s
tweaking edge_append_loc_nil
CI #657: Commit 9474415 pushed by m4lvin
September 20, 2024 21:38 4m 7s main
September 20, 2024 21:38 4m 7s
one easy sorry in loadedDiamondPaths
CI #656: Commit e1b88aa pushed by m4lvin
September 20, 2024 17:00 4m 6s main
September 20, 2024 17:00 4m 6s
prove cp3a
CI #655: Commit a2fb0a7 pushed by m4lvin
September 19, 2024 22:14 4m 19s main
September 19, 2024 22:14 4m 19s
make FL closed under single negations etc.
CI #654: Commit c81b970 pushed by m4lvin
September 18, 2024 10:31 4m 6s flHom
September 18, 2024 10:31 4m 6s
make FL closed under single negations etc.
CI #653: Commit 1dd58ea pushed by m4lvin
September 18, 2024 07:34 4m 18s flHom
September 18, 2024 07:34 4m 18s
alternative def of FL() via OrderHom.nextFixed
CI #652: Commit c51a38b pushed by m4lvin
September 17, 2024 22:12 4m 16s flHom
September 17, 2024 22:12 4m 16s
correction to Qtests, proof pieces for cp3a
CI #651: Commit 0820eb9 pushed by m4lvin
September 17, 2024 14:00 4m 3s main
September 17, 2024 14:00 4m 3s
cp3a statement
CI #650: Commit 8707c8c pushed by m4lvin
September 17, 2024 13:07 4m 1s main
September 17, 2024 13:07 4m 1s
[main]: correction to which inductionOn is used yet
Codespaces Prebuilds #51: by github-codespaces bot
September 16, 2024 06:00 17m 12s
September 16, 2024 06:00 17m 12s
attempt for Fintype PathIn
CI #649: Commit 49a9c40 pushed by m4lvin
September 13, 2024 21:47 3m 58s PathIn-Fintype
September 13, 2024 21:47 3m 58s