Skip to content

Actions: m4lvin/lean4-pdl

Actions

CI

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
786 workflow runs
786 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

Finish proof of relate_existsH_distance
CI #837: Commit 484cd36 pushed by Noam-Coh3n
January 22, 2025 15:17 5m 6s distance-walks
January 22, 2025 15:17 5m 6s
Finish proof of relate_existsH_distance
CI #836: Commit 67762b2 pushed by Noam-Coh3n
January 22, 2025 15:06 5m 9s distance-walks
January 22, 2025 15:06 5m 9s
idea for ⋖_ converse well-foundednes
CI #835: Commit 56789c5 pushed by m4lvin
January 21, 2025 21:53 3m 17s PathIn-Fintype
January 21, 2025 21:53 3m 17s
add placeholders
CI #834: Commit 4cd6086 pushed by m4lvin
January 21, 2025 19:47 3m 20s bml-bisimulation
January 21, 2025 19:47 3m 20s
attempt for Fintype PathIn
CI #833: Commit 3220ff3 pushed by m4lvin
January 21, 2025 14:54 3m 11s PathIn-Fintype
January 21, 2025 14:54 3m 11s
move Path and Vector stuff out of Soundness.lean
CI #832: Commit 4e71704 pushed by m4lvin
January 21, 2025 14:26 3m 57s main
January 21, 2025 14:26 3m 57s
rename rep to lrep
CI #831: Commit da05e86 pushed by m4lvin
January 21, 2025 11:31 4m 2s main
January 21, 2025 11:31 4m 2s
rename rep to lrep
CI #830: Commit da05e86 pushed by m4lvin
January 21, 2025 11:31 3m 32s basic-non-basic
January 21, 2025 11:31 3m 32s
Almost there, one sorry left in relate_existsH_distance
CI #829: Commit fb9f64e pushed by Noam-Coh3n
January 21, 2025 01:19 4m 58s distance-walks
January 21, 2025 01:19 4m 58s
Fix some definitions and prove more helper theorems
CI #828: Commit b8c8904 pushed by Noam-Coh3n
January 20, 2025 22:33 4m 53s distance-walks
January 20, 2025 22:33 4m 53s
WIP to define loadedSucc
CI #827: Commit 17a090b pushed by m4lvin
January 19, 2025 13:27 4m 22s loadPathsTry
January 19, 2025 13:27 4m 22s
define Sequent.basic to imply "not closed"
CI #826: Commit e8d36c6 pushed by m4lvin
January 19, 2025 12:14 3m 18s basic-non-basic
January 19, 2025 12:14 3m 18s
January 17, 2025 15:44 4m 58s
January 16, 2025 23:32 4m 52s
Finished proof of relateSeq_H_imp_relate
CI #823: Commit 553bc3f pushed by Noam-Coh3n
January 16, 2025 21:16 5m 13s distance-walks
January 16, 2025 21:16 5m 13s
Prove ;'-case of relateSeq_H_imp_relate
CI #822: Commit 8ceec3a pushed by Noam-Coh3n
January 16, 2025 17:00 5m 1s distance-walks
January 16, 2025 17:00 5m 1s
WIP add TableauExamples
CI #821: Commit b6a5488 pushed by m4lvin
January 16, 2025 15:19 3m 29s basic-non-basic
January 16, 2025 15:19 3m 29s
Adding theorem relateSeq_H_imp_relate
CI #820: Commit bb6462e pushed by Noam-Coh3n
January 16, 2025 15:13 4m 55s distance-walks
January 16, 2025 15:13 4m 55s
make ⊥ non-basic
CI #819: Commit fdacf96 pushed by m4lvin
January 16, 2025 12:03 3m 13s basic-non-basic
January 16, 2025 12:03 3m 13s
make ⊥ non-basic
CI #818: Commit 68c7bc1 pushed by m4lvin
January 16, 2025 11:44 3m 14s basic-non-basic
January 16, 2025 11:44 3m 14s
add Tableau conditions for (non-)basic and no-repeat
CI #817: Commit b109de4 pushed by m4lvin
January 16, 2025 11:37 3m 30s basic-non-basic
January 16, 2025 11:37 3m 30s
add Tableau conditions for (non-)basic and no-repeat
CI #816: Commit b0de1aa pushed by m4lvin
January 15, 2025 19:30 3m 22s basic-non-basic
January 15, 2025 19:30 3m 22s
WIP add Tableau conditions for (non-)basic and no-repeat
CI #815: Commit 4fc5001 pushed by m4lvin
January 15, 2025 17:42 4m 41s basic-non-basic
January 15, 2025 17:42 4m 41s
Prove union case of relate_existsH_distance
CI #814: Commit 7cb2f2a pushed by Noam-Coh3n
January 15, 2025 16:58 3m 22s distance-walks
January 15, 2025 16:58 3m 22s
List website content in CI
CI #813: Commit 1de8730 pushed by m4lvin
January 15, 2025 16:37 12m 46s main
January 15, 2025 16:37 12m 46s