Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions content/docs/class_reps/alt.v
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ NES.Begin Point.

Consider the following AST `source`, definining C++ class `Point`.
|*)
#[elaborate]
cpp.prog source prog cpp:{{
class Point {
int x;
Expand Down Expand Up @@ -97,6 +98,7 @@ To continue, we abort the proof, and define AST `source1` with a fixed version o
|*)
Abort.

#[elaborate]
cpp.prog source1 prog cpp:{{
class Point {
int x{0};
Expand Down
1 change: 1 addition & 0 deletions content/docs/class_reps/main.v
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ Require Import skylabs.lang.cpp.parser.plugin.cpp2v.
## The Program

Here, we define the AST `source` containing our example C++ program: |*)
#[elaborate]
cpp.prog source prog cpp:{{
struct IntCell {
int n{0};
Expand Down
1 change: 1 addition & 0 deletions content/docs/rep_hints/main.v
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ Require Import skylabs.lang.cpp.parser.plugin.cpp2v.

(*| Define AST `source` containing our example C++ program.
This is the same as in the [earlier tutorial](../../class_reps/main). |*)
#[elaborate]
cpp.prog source prog cpp:{{
struct IntCell {
int n{0};
Expand Down