Skip to content

Proof decomposition by template. - #268

Open
kape1395 wants to merge 9 commits into
mainfrom
lsp-decompose-proof-tpl
Open

Proof decomposition by template.#268
kape1395 wants to merge 9 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.

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
@kape1395
kape1395 marked this pull request as ready for review August 10, 2026 21:04
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