From bf0b35b9b1fa90d50587e906432077b63a9ad34d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 11 Mar 2024 09:43:21 +0100
Subject: Update the generated files

---
 tests/fstar/demo/Demo.fst | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tests/fstar/demo')

diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index f9082979..22322ee7 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -121,14 +121,14 @@ let rec i32_id (n : nat) (i : i32) : result i32 =
     Source: 'src/demo.rs', lines 83:0-83:17 *)
 noeq type counter_t (self : Type0) = { incr : self -> result (usize & self); }
 
-(** [demo::{usize}::incr]:
+(** [demo::{(demo::Counter for usize)}::incr]:
     Source: 'src/demo.rs', lines 88:4-88:31 *)
-let usize_incr (self : usize) : result (usize & usize) =
+let counterUsize_incr (self : usize) : result (usize & usize) =
   let* self1 = usize_add self 1 in Return (self, self1)
 
-(** Trait implementation: [demo::{usize}]
+(** Trait implementation: [demo::{(demo::Counter for usize)}]
     Source: 'src/demo.rs', lines 87:0-87:22 *)
-let demo_CounterUsizeInst : counter_t usize = { incr = usize_incr; }
+let counterUsize : counter_t usize = { incr = counterUsize_incr; }
 
 (** [demo::use_counter]:
     Source: 'src/demo.rs', lines 95:0-95:59 *)
-- 
cgit v1.2.3


From 21fdbab049534b35e9573da89bdfd5942144cbb9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 11 Mar 2024 10:20:15 +0100
Subject: Regenerate the test files

---
 tests/fstar/demo/Demo.fst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tests/fstar/demo')

diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index 22322ee7..d13d2ba3 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -133,6 +133,6 @@ let counterUsize : counter_t usize = { incr = counterUsize_incr; }
 (** [demo::use_counter]:
     Source: 'src/demo.rs', lines 95:0-95:59 *)
 let use_counter
-  (t : Type0) (counterTInst : counter_t t) (cnt : t) : result (usize & t) =
-  counterTInst.incr cnt
+  (t : Type0) (counterInst : counter_t t) (cnt : t) : result (usize & t) =
+  counterInst.incr cnt
 
-- 
cgit v1.2.3