Skip to content

Pull requests: leanprover/cslib

New pull request New
68 Open 488 Closed
68 Open 488 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

feat(Automata, LTS, TM): Introduce LTS.SMTr and LTS.mapLabel, generalise TM tapes to arbitrary universes, fix EpsilonNA, and introduce their single-accept transformation automata
#625 opened Jun 10, 2026 by fmontesi Collaborator Loading…
feat(FLP): show that asynchronous distributed consensus is possible when there is no fault
#619 opened Jun 5, 2026 by ctchou Collaborator Loading…
2
feat(Automata, LTS, and Turing): saturated multistep transitions, mapLabel for LTS, and Nondeterministic Turing Machines (NTM)
#615 opened Jun 4, 2026 by fmontesi Collaborator Loading…
3
feat(FLP): some technical machineries for reasoning about diamond and fairness properties
#612 opened Jun 1, 2026 by ctchou Collaborator Loading…
8
feat(Logic): logical operators
#607 opened May 29, 2026 by fmontesi Collaborator Loading…
7
feat(Algorithms/Lean/MergeSort): relate mergeSort to List.mergeSort
#605 opened May 28, 2026 by exekis Loading…
feat(Control/Monad): Weakest preconditions and mcvgen for free monads
#604 opened May 28, 2026 by tannerduve Contributor Loading…
10
feat(LTS): labeled transition systems as coalgebras
#603 opened May 28, 2026 by tannerduve Contributor Loading…
feat(Foundations/Combinatorics/BooleanFunctions): Fourier expansion, Plancherel, and Parseval
#596 opened May 23, 2026 by SamuelSchlesinger Collaborator Loading…
9
feat(Computability): Abstract machine model.
#595 opened May 23, 2026 by crei • Draft
3
feat(Computability): introduce TapeEncodable class for Turing machine types
#591 opened May 21, 2026 by Sfgangloff Loading…
9
feat(Foundations/Logic): Notation typeclasses and models
#587 opened May 21, 2026 by thomaskwaring Collaborator • Draft
4
feat: parallel substitution typeclass; refactor strong normalization
#583 opened May 20, 2026 by WegmannDavid Contributor Loading…
feat(Crypto): Generalize encryption schemes over arbitrary monads
#581 opened May 20, 2026 by dtumad Loading…
6
feat(algorithms): add counting sort
#577 opened May 19, 2026 by Robertboy18 Loading…
7
feat(algorithms): add stable insertion sort
#576 opened May 19, 2026 by Robertboy18 Loading…
5
feat(algorithms): add stable bubble sort
#575 opened May 19, 2026 by Robertboy18 Loading…
3
feat: Splay Tree Formalisation
#568 opened May 16, 2026 by AntoineduFresne Loading…
27
simple functional queue from Okasaki
#558 opened May 11, 2026 by c-cube Loading…
26
feat(Algorithms): verify minScan (list minimum) with TimeM cost modelAdded new feat MinList
#554 opened May 8, 2026 by Noobmaster-IIIT Loading…
feat(Algorithms/Lean): add timed insertion sort
#553 opened May 8, 2026 by ps600779 Loading…
2
Start general definitions for computation models
#550 opened May 6, 2026 by kesslermaximilian Loading…
8
feat(Logics/Propositional): further API for manipulating theories in natural deduction
#542 opened May 4, 2026 by thomaskwaring Collaborator Loading…
feat(Boole): Bring Boole sandbox to Lean 4.29 and add queue examples
#539 opened May 3, 2026 by Robertboy18 Loading…
6
refactor(Logics/Propositional): classical and intuitionistic inference systems
#536 opened May 2, 2026 by thomaskwaring Collaborator Loading…
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.