Category
Lean formalization
Describe the feature you'd like to request
In the Rust implementation of SymCC, cedar-policy/cedar#1846, cedar-policy/cedar#1849, cedar-policy/cedar#1857 kill the solver process and let OS recollect it when the solver reports a parsing error or reading its output encounters an EOF. Note that it's for CVC5 only.
We can't seem to port these changes readily because Rust uses a trait to represent solvers and Lean uses a type. So I create an issue instead.
Describe alternatives you've considered
N/A
Additional context
No response
Is this something that you'd be interested in working on?
Category
Lean formalization
Describe the feature you'd like to request
In the Rust implementation of SymCC, cedar-policy/cedar#1846, cedar-policy/cedar#1849, cedar-policy/cedar#1857 kill the solver process and let OS recollect it when the solver reports a parsing error or reading its output encounters an EOF. Note that it's for CVC5 only.
We can't seem to port these changes readily because Rust uses a trait to represent solvers and Lean uses a type. So I create an issue instead.
Describe alternatives you've considered
N/A
Additional context
No response
Is this something that you'd be interested in working on?