Skip to content

Proof decomposition by template.#268

Draft
kape1395 wants to merge 2 commits into
mainfrom
lsp-decompose-proof-tpl
Draft

Proof decomposition by template.#268
kape1395 wants to merge 2 commits into
mainfrom
lsp-decompose-proof-tpl

Conversation

@kape1395
Copy link
Copy Markdown
Collaborator

Extensible proof decomposition rules.

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395 kape1395 self-assigned this May 11, 2026
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
Copy link
Copy Markdown
Collaborator Author

@uguryavuz, that's the branch I was working on. The match function is implemented only partially, for a PoC. Tried to rewrite it using existing visitors, but probably will stick with explicit traversal using a recursive function.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

1 participant