Skip to content

Pull requests: leanprover/cslib

New pull request New
75 Open 474 Closed
75 Open 474 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

chore: Bump mathlib dependency to 2ba98ca
#634 opened Jun 11, 2026 by mathlib-nightly-testing Bot Loading…
feat(Foundations/Logic, Logics/Propositional): Hilbert proof systems, metalogic, ND equivalence, and Kripke semantics
#633 opened Jun 11, 2026 by benbrastmckie Loading…
@arademaker
2
chore: split the Relation module
#632 opened Jun 11, 2026 by chenson2018 Collaborator Loading…
3
chore: bump mathlib to 8589236, fix breaking changes dependency-incompatibility-fix Fix PR for a dependency incompatibility, opened by downstream-reports
#628 opened Jun 10, 2026 by mathlib-nightly-testing Bot Loading…
1
doc: add wikidata attribute for Church-Rosser theorems
#626 opened Jun 10, 2026 by chenson2018 Collaborator Loading…
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
chore(LTS): add API for TraceEq and relatives
#617 opened Jun 5, 2026 by thomaskwaring Collaborator Loading…
1 task
16
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
ProTip! no:milestone will show everything without a milestone.