Update the guide

creusot-rs · Nov 28, 2024 · 0c92f7f · 0c92f7f
1 parent 118c7eb
commit 0c92f7f
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/guide/src/SUMMARY.md b/guide/src/SUMMARY.md
@@ -17,4 +17,5 @@
 - [Snapshots](snapshots.md)
 - [Ghost code](ghost.md)
   - [Ghost structures](ghost/ghost-structures.md)
+  - [`Int` in ghost](ghost/int-in-ghost.md)
 - [Type invariants](./type_invariants.md)
diff --git a/guide/src/ghost/int-in-ghost.md b/guide/src/ghost/int-in-ghost.md
@@ -0,0 +1,11 @@
+# Int in ghost
+
+You can manipulate values of type `Int` in ghost code, by using the `int` suffix on integer literals:
+
+```rust,creusot
+ghost! {
+    let my_int = 42int;
+};
+```
+
+Right now you cannot do much except pass it around: operations like `+` or `*` are only supported in pearlite.