Skip to content

Pull requests: leanprover/cslib

New pull request New
95 Open 554 Closed
95 Open 554 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

fix: remove grind attr from Xi.step_lc_r
#751 opened Jul 26, 2026 by lengyijun Contributor Loading…
refactor: Add Xi.step_lc_l and simplify step_lc_l in FullBeta/FullEta
#750 opened Jul 26, 2026 by lengyijun Contributor Loading…
fix: Simplify FullEta.step_lc_r proof
#749 opened Jul 26, 2026 by lengyijun Contributor Loading…
fix(LTS): define acyclicity by well-founded termination
#748 opened Jul 25, 2026 by SamuelSchlesinger Collaborator Loading…
5
fix(PACLearning): restrict consistency to realizable samples
#747 opened Jul 25, 2026 by SamuelSchlesinger Collaborator Loading…
fix(Modal): combine frame conditions in modal cube
#746 opened Jul 25, 2026 by SamuelSchlesinger Collaborator Loading…
feat(LambdaCalculus/Named/Untyped): Alpha equivalence equalities
#741 opened Jul 22, 2026 by chris-anto-froeschl Contributor Loading…
@chenson2018
refactor: remove FullBeta.step_subst_cong_r
#738 opened Jul 21, 2026 by lengyijun Contributor Loading…
@chenson2018
test(LambdaCalculus): add tests for capture-avoiding substitution
#737 opened Jul 21, 2026 by korbonits Loading…
1
@chenson2018
1
feat: Add lemma SN.to_WN: SN implies Normalizable
#736 opened Jul 21, 2026 by lengyijun Contributor Loading…
@chenson2018
2
refactor(LocallyNameless): remove unnecessary LC assumptions
#735 opened Jul 21, 2026 by lengyijun Contributor Loading…
@chenson2018
1
feat(LocallyNameless/Untyped): add FullEta.steps_lc_l
#734 opened Jul 21, 2026 by lengyijun Contributor Loading…
@chenson2018
feat(PFunctor): redefine PFunctor.FreeM in terms of PFunctor.W
#731 opened Jul 18, 2026 by dtumad Loading…
feat(StackTape): lemmas for mapSome
#726 opened Jul 17, 2026 by BoltonBailey Contributor • Draft
chore: clean imports
#725 opened Jul 17, 2026 by felixpernegger Contributor Loading…
8
feat(FLP): define pseudo-consensus and prove that it is implied by consensus
#718 opened Jul 13, 2026 by ctchou Collaborator Loading…
feat(Data/PFunctor): extend free monad and M-type APIs
#716 opened Jul 13, 2026 by dtumad Loading…
refactor(Locallynameless): Multiapp => List.foldl
#710 opened Jul 12, 2026 by lengyijun Contributor Loading…
@chenson2018
5
feat(LocallyNameless/Untyped): FullEta.steps_open_cong_l
#705 opened Jul 10, 2026 by lengyijun Contributor Loading…
@chenson2018
1
feat: topological characterization of safety and liveness properties of infinite sequences
#704 opened Jul 9, 2026 by ctchou Collaborator Loading…
feat(untyped): the Leftmost Reduction Theorem
#700 opened Jul 8, 2026 by m-ow Contributor Loading…
@chenson2018
51
feat(UnionFind): union by rank with verified O(log n) find
#695 opened Jul 1, 2026 by barni120400 Loading…
feat(Algorithms/Graph): add Floyd-Warshall invariant
#691 opened Jul 1, 2026 by FawadHa1der Loading…
3
feat(Computability): add quantum computing foundations
#689 opened Jul 1, 2026 by exAClior Loading…
4 tasks done
1
2
feat: query complexity model with combined history
#685 opened Jun 30, 2026 by Shreyas4991 Contributor Loading…
ProTip! no:milestone will show everything without a milestone.