From 1fa2fa7e9e029f0e5b492fdb5829cd99fa340eee Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gregory@skylabs-ai.com>
Date: Wed, 11 Feb 2026 23:28:57 -0500
Subject: [PATCH] Explicitly add [#[elaborate]] attribute.

---
 content/docs/class_reps/alt.v  | 2 ++
 content/docs/class_reps/main.v | 1 +
 content/docs/rep_hints/main.v  | 1 +
 3 files changed, 4 insertions(+)

diff --git a/content/docs/class_reps/alt.v b/content/docs/class_reps/alt.v
index 61c4a01..31a0bc2 100644
--- a/content/docs/class_reps/alt.v
+++ b/content/docs/class_reps/alt.v
@@ -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;
@@ -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};
diff --git a/content/docs/class_reps/main.v b/content/docs/class_reps/main.v
index 62160b8..d9bcd83 100644
--- a/content/docs/class_reps/main.v
+++ b/content/docs/class_reps/main.v
@@ -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};
diff --git a/content/docs/rep_hints/main.v b/content/docs/rep_hints/main.v
index 6601daa..f1445d3 100644
--- a/content/docs/rep_hints/main.v
+++ b/content/docs/rep_hints/main.v
@@ -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};