Skip to content

Pull requests: GoelandProver/Goeland

New pull request New
7 Open 56 Closed
7 Open 56 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: De-Bruijn Style Nameless Bound Variables kind:cleanup Refactoring or improvement of existing code kind:enhancement New feature or upgrade of a previous one needs:rebase When the PR needs to get rebased in order to get merged part:ast
#79 opened Mar 26, 2026 by jrosain Member Loading…
Allow unification between terms kind:cleanup Refactoring or improvement of existing code part:unification About the unification process of Goéland
#78 opened Mar 26, 2026 by jrosain Member Loading…
feat: remove invasive index in formulas and terms has:other-pr-dependency This PR cannot be merged before another PR (the maintainer should specify the dependency(ies)) kind:cleanup Refactoring or improvement of existing code needs:ci Needs a CI run before merging needs:rebase When the PR needs to get rebased in order to get merged
#71 opened Mar 20, 2026 by jrosain Member Loading…
fix: deskolemization algorithm has:other-pr-dependency This PR cannot be merged before another PR (the maintainer should specify the dependency(ies)) kind:cleanup Refactoring or improvement of existing code kind:fix The PR fixes a bug needs:rebase When the PR needs to get rebased in order to get merged part:lambdapi-output part:proof-output About the vanilla proof output (in custom format) part:rocq-output About the certified output in Rocq
#70 opened Mar 10, 2026 by jrosain Member Loading… 1.2
1
Improve formatting by using golines kind:request Requesting a new feature needs:discussion The PR needs to be discussed needs:rebase When the PR needs to get rebased in order to get merged part:infrastructure The PR is on non-goéland code
#69 opened Feb 22, 2026 by jrosain Member • Draft
Fix lambdapi output by updating it with the new printer system kind:cleanup Refactoring or improvement of existing code kind:fix The PR fixes a bug part:lambdapi-output
#67 opened Oct 8, 2025 by jrosain Member Loading… 1.2
@jcailler
Add IProof interface with a tree structure and add relevant adapter for []Search.ProofStruct has:other-pr-dependency This PR cannot be merged before another PR (the maintainer should specify the dependency(ies)) kind:enhancement New feature or upgrade of a previous one needs:ci Needs a CI run before merging needs:rebase When the PR needs to get rebased in order to get merged part:proof-output About the vanilla proof output (in custom format)
#64 opened Sep 1, 2025 by jrosain Member Loading… 1.2
@jcailler
1
ProTip! no:milestone will show everything without a milestone.