From 586d631f09bb4d2ec9bab53b93e8a96c9bc618f9 Mon Sep 17 00:00:00 2001
From: Jay Lorch <jaylorch@gmail.com>
Date: Tue, 3 Mar 2026 16:46:09 -0800
Subject: [PATCH] Got cargo build working

---
 src/number.rs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/number.rs b/src/number.rs
index 703729a..fc910d3 100644
--- a/src/number.rs
+++ b/src/number.rs
@@ -61,11 +61,13 @@ pub assume_specification[ <Number as Clone>::clone ](n: &Number) -> (res: Number
         res == n,
 ;
 
+#[cfg(verus_keep_ghost)]
 pub enum NumberView {
     Integer(int),
     Float(f64),
 }
 
+#[cfg(verus_keep_ghost)]
 impl View for Number
 {
     type V = NumberView;