Pull requests · leanprover/cslib · GitHub
Skip to content

Pull requests: leanprover/cslib

New pull request New
77 Open 509 Closed
77 Open 509 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: fix the header of Cslib/Computability/Automata/DA/Prod.lean
#682 opened Jun 26, 2026 by ctchou Collaborator Loading…
feat(untyped): standardization theorem for the lambda calculus
#679 opened Jun 24, 2026 by m-ow Contributor Loading…
refactor(LocallyNameless/Untyped): rename close_open => close_openRec
#678 opened Jun 24, 2026 by lengyijun Contributor Loading…
chore: auto-merge lake update PRs
#676 opened Jun 23, 2026 by buyolitsez Loading…
1
fix(Foundations): add noWs guard to well-formed postfix notation
#675 opened Jun 22, 2026 by VitaliPath Loading…
3
perf: try fixing the Subtype.weaken proof
#674 opened Jun 22, 2026 by chenson2018 Collaborator • Draft
2
refactor(LocallyNameless/Untyped): Rename redex_abs_close to steps_abs_close
#672 opened Jun 21, 2026 by lengyijun Contributor Loading…
1
feat(Logics/Modal): refactor formula primitives to {atom, bot, imp, box}
#662 opened Jun 19, 2026 by benbrastmckie Loading…
feat: basic defs of collections of labelled transition systems
#661 opened Jun 18, 2026 by Shreyas4991 Contributor • Draft
9
feat(Foundations/Data): lawful lenses for verified state access
#659 opened Jun 17, 2026 by fraware • Draft
4 tasks
feat(Logics/LTL): LTL formula type and semantics over omega-words
#649 opened Jun 15, 2026 by benbrastmckie Loading…
11
feat(Logics/Propositional): five-primitive formula type with primitive bot
#648 opened Jun 14, 2026 by benbrastmckie Loading…
3
chore: Bump mathlib dependency to 4364cad
#645 opened Jun 13, 2026 by mathlib-nightly-testing Bot Loading…
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…
12
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…
30
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
5
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
ProTip! Type g i on any issue or pull request to go back to the issue listing page.