Closed junkil-park closed 1 year ago
A type parameter that has the key-ability can have a memory space. This PR makes Prover declare the memory variables for type parameters in the generated boogie file.
To declare the memory variables for type parameters
yes
cargo test
A type parameter that has the key-ability can have a memory space. This PR makes Prover declare the memory variables for type parameters in the generated boogie file.
Motivation
To declare the memory variables for type parameters
Have you read the Contributing Guidelines on pull requests?
yes
Test Plan
cargo test