Dataclass

The command cpp.class automatically generates Rep predicate, specifications, as well as proofs for data classes, including structs.

Contents

• main.cpp
• main_proof.v