From df4d60b71bcabf9897656d6d74157a4c7d8d539c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 16 May 2023 11:45:43 +0200
Subject: Make good progress on generating code for HOL4

---
 tests/coq/betree/BetreeMain_Funs.v | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'tests/coq/betree')

diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index dc97a9e9..940b8650 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -56,7 +56,7 @@ Definition betree_fresh_node_id_back (counter : u64) : result u64 :=
 
 (** [betree_main::betree::NodeIdCounter::{0}::new] *)
 Definition betree_node_id_counter_new_fwd : result Betree_node_id_counter_t :=
-  Return {| Betree_node_id_counter_next_node_id := (0%u64) |}
+  Return {| Betree_node_id_counter_next_node_id := 0%u64 |}
 .
 
 (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
@@ -75,7 +75,7 @@ Definition betree_node_id_counter_fresh_id_back
 
 (** [core::num::u64::{10}::MAX] *)
 Definition core_num_u64_max_body : result u64 :=
-  Return (18446744073709551615%u64)
+  Return 18446744073709551615%u64
 .
 Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global.
 
@@ -86,7 +86,7 @@ Definition betree_upsert_update_fwd
   | None =>
     match st with
     | BetreeUpsertFunStateAdd v => Return v
-    | BetreeUpsertFunStateSub i => Return (0%u64)
+    | BetreeUpsertFunStateSub i => Return 0%u64
     end
   | Some prev0 =>
     match st with
@@ -94,7 +94,7 @@ Definition betree_upsert_update_fwd
       margin <- u64_sub core_num_u64_max_c prev0;
       if margin s>= v then u64_add prev0 v else Return core_num_u64_max_c
     | BetreeUpsertFunStateSub v =>
-      if prev0 s>= v then u64_sub prev0 v else Return (0%u64)
+      if prev0 s>= v then u64_sub prev0 v else Return 0%u64
     end
   end
 .
@@ -107,7 +107,7 @@ Fixpoint betree_list_len_fwd
   | S n0 =>
     match self with
     | BetreeListCons t tl => i <- betree_list_len_fwd T n0 tl; u64_add 1%u64 i
-    | BetreeListNil => Return (0%u64)
+    | BetreeListNil => Return 0%u64
     end
   end
 .
@@ -1061,8 +1061,7 @@ Definition betree_be_tree_new_fwd
         |};
       Betree_be_tree_node_id_cnt := node_id_cnt0;
       Betree_be_tree_root :=
-        (BetreeNodeLeaf
-          {| Betree_leaf_id := id; Betree_leaf_size := (0%u64) |})
+        (BetreeNodeLeaf {| Betree_leaf_id := id; Betree_leaf_size := 0%u64 |})
     |})
 .
 
-- 
cgit v1.2.3