Use short names for the structure fields in Lean

8 files changed, 154 insertions, 248 deletions

diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 41e4349e..b0939155 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -48,23 +48,20 @@ def betree.fresh_node_id_back (counter : U64) : Result U64 :=
 
 /- [betree_main::betree::NodeIdCounter::{0}::new]: forward function -/
 def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
-  Result.ret
-  { betree_node_id_counter_next_node_id := (U64.ofInt 0 (by intlit)) }
+  Result.ret { next_node_id := (U64.ofInt 0 (by intlit)) }
 
 /- [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function -/
 def betree.NodeIdCounter.fresh_id (self : betree.NodeIdCounter) : Result U64 :=
   do
-    let _ ← self.betree_node_id_counter_next_node_id +
-      (U64.ofInt 1 (by intlit))
-    Result.ret self.betree_node_id_counter_next_node_id
+    let _ ← self.next_node_id + (U64.ofInt 1 (by intlit))
+    Result.ret self.next_node_id
 
 /- [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 -/
 def betree.NodeIdCounter.fresh_id_back
   (self : betree.NodeIdCounter) : Result betree.NodeIdCounter :=
   do
-    let i ← self.betree_node_id_counter_next_node_id +
-      (U64.ofInt 1 (by intlit))
-    Result.ret { betree_node_id_counter_next_node_id := i }
+    let i ← self.next_node_id + (U64.ofInt 1 (by intlit))
+    Result.ret { next_node_id := i }
 
 /- [core::num::u64::{10}::MAX] -/
 def core_num_u64_max_body : Result U64 :=
@@ -181,8 +178,7 @@ def betree.Leaf.split
   Result (State × betree.Internal)
   :=
   do
-    let p ←
-      betree.List.split_at (U64 × U64) content params.betree_params_split_size
+    let p ← betree.List.split_at (U64 × U64) content params.split_size
     let (content0, content1) := p
     let p0 ← betree.List.hd (U64 × U64) content1
     let (pivot, _) := p0
@@ -191,17 +187,9 @@ def betree.Leaf.split
     let id1 ← betree.NodeIdCounter.fresh_id node_id_cnt0
     let (st0, _) ← betree.store_leaf_node id0 content0 st
     let (st1, _) ← betree.store_leaf_node id1 content1 st0
-    let n := betree.Node.Leaf
-      {
-        betree_leaf_id := id0,
-        betree_leaf_size := params.betree_params_split_size
-      }
-    let n0 := betree.Node.Leaf
-      {
-        betree_leaf_id := id1,
-        betree_leaf_size := params.betree_params_split_size
-      }
-    Result.ret (st1, betree.Internal.mk self.betree_leaf_id pivot n n0)
+    let n := betree.Node.Leaf { id := id0, size := params.split_size }
+    let n0 := betree.Node.Leaf { id := id1, size := params.split_size }
+    Result.ret (st1, betree.Internal.mk self.id pivot n n0)
 
 /- [betree_main::betree::Leaf::{3}::split]: backward function 2 -/
 def betree.Leaf.split_back
@@ -210,8 +198,7 @@ def betree.Leaf.split_back
   Result betree.NodeIdCounter
   :=
   do
-    let p ←
-      betree.List.split_at (U64 × U64) content params.betree_params_split_size
+    let p ← betree.List.split_at (U64 × U64) content params.split_size
     let (content0, content1) := p
     let _ ← betree.List.hd (U64 × U64) content1
     let id0 ← betree.NodeIdCounter.fresh_id node_id_cnt
@@ -392,7 +379,7 @@ mutual divergent def betree.Node.lookup
           Result.ret (st1, opt)
   | betree.Node.Leaf node =>
     do
-      let (st0, bindings) ← betree.load_leaf_node node.betree_leaf_id st
+      let (st0, bindings) ← betree.load_leaf_node node.id st
       let opt ← betree.Node.lookup_in_bindings key bindings
       Result.ret (st0, opt)
 
@@ -463,7 +450,7 @@ divergent def betree.Node.lookup_back
           Result.ret (betree.Node.Internal node0)
   | betree.Node.Leaf node =>
     do
-      let (_, bindings) ← betree.load_leaf_node node.betree_leaf_id st
+      let (_, bindings) ← betree.load_leaf_node node.id st
       let _ ← betree.Node.lookup_in_bindings key bindings
       Result.ret (betree.Node.Leaf node)
 
@@ -732,7 +719,7 @@ mutual divergent def betree.Node.apply_messages
       let (st0, content) ← betree.load_internal_node i st
       let content0 ← betree.Node.apply_messages_to_internal content msgs
       let num_msgs ← betree.List.len (U64 × betree.Message) content0
-      if num_msgs >= params.betree_params_min_flush_size
+      if num_msgs >= params.min_flush_size
       then
         do
           let (st1, content1) ←
@@ -750,22 +737,20 @@ mutual divergent def betree.Node.apply_messages
           Result.ret (st1, ())
   | betree.Node.Leaf node =>
     do
-      let (st0, content) ← betree.load_leaf_node node.betree_leaf_id st
+      let (st0, content) ← betree.load_leaf_node node.id st
       let content0 ← betree.Node.apply_messages_to_leaf content msgs
       let len ← betree.List.len (U64 × U64) content0
-      let i ← (U64.ofInt 2 (by intlit)) * params.betree_params_split_size
+      let i ← (U64.ofInt 2 (by intlit)) * params.split_size
       if len >= i
       then
         do
           let (st1, _) ←
             betree.Leaf.split node content0 params node_id_cnt st0
-          let (st2, _) ←
-            betree.store_leaf_node node.betree_leaf_id betree.List.Nil st1
+          let (st2, _) ← betree.store_leaf_node node.id betree.List.Nil st1
           Result.ret (st2, ())
       else
         do
-          let (st1, _) ←
-            betree.store_leaf_node node.betree_leaf_id content0 st0
+          let (st1, _) ← betree.store_leaf_node node.id content0 st0
           Result.ret (st1, ())
 
 /- [betree_main::betree::Node::{5}::apply_messages]: backward function 0 -/
@@ -782,7 +767,7 @@ divergent def betree.Node.apply_messages_back
       let (st0, content) ← betree.load_internal_node i st
       let content0 ← betree.Node.apply_messages_to_internal content msgs
       let num_msgs ← betree.List.len (U64 × betree.Message) content0
-      if num_msgs >= params.betree_params_min_flush_size
+      if num_msgs >= params.min_flush_size
       then
         do
           let (st1, content1) ←
@@ -802,25 +787,23 @@ divergent def betree.Node.apply_messages_back
             node_id_cnt)
   | betree.Node.Leaf node =>
     do
-      let (st0, content) ← betree.load_leaf_node node.betree_leaf_id st
+      let (st0, content) ← betree.load_leaf_node node.id st
       let content0 ← betree.Node.apply_messages_to_leaf content msgs
       let len ← betree.List.len (U64 × U64) content0
-      let i ← (U64.ofInt 2 (by intlit)) * params.betree_params_split_size
+      let i ← (U64.ofInt 2 (by intlit)) * params.split_size
       if len >= i
       then
         do
           let (st1, new_node) ←
             betree.Leaf.split node content0 params node_id_cnt st0
-          let _ ←
-            betree.store_leaf_node node.betree_leaf_id betree.List.Nil st1
+          let _ ← betree.store_leaf_node node.id betree.List.Nil st1
           let node_id_cnt0 ←
             betree.Leaf.split_back node content0 params node_id_cnt st0
           Result.ret (betree.Node.Internal new_node, node_id_cnt0)
       else
         do
-          let _ ← betree.store_leaf_node node.betree_leaf_id content0 st0
-          Result.ret (betree.Node.Leaf { node with betree_leaf_size := len },
-            node_id_cnt)
+          let _ ← betree.store_leaf_node node.id content0 st0
+          Result.ret (betree.Node.Leaf { node with size := len }, node_id_cnt)
 
 /- [betree_main::betree::Internal::{4}::flush]: forward function -/
 divergent def betree.Internal.flush
@@ -834,7 +817,7 @@ divergent def betree.Internal.flush
     let p ← betree.List.partition_at_pivot betree.Message content i
     let (msgs_left, msgs_right) := p
     let len_left ← betree.List.len (U64 × betree.Message) msgs_left
-    if len_left >= params.betree_params_min_flush_size
+    if len_left >= params.min_flush_size
     then
       do
         let (st0, _) ←
@@ -842,7 +825,7 @@ divergent def betree.Internal.flush
         let (_, node_id_cnt0) ←
           betree.Node.apply_messages_back n params node_id_cnt msgs_left st
         let len_right ← betree.List.len (U64 × betree.Message) msgs_right
-        if len_right >= params.betree_params_min_flush_size
+        if len_right >= params.min_flush_size
         then
           do
             let (st1, _) ←
@@ -872,7 +855,7 @@ divergent def betree.Internal.flush_back
     let p ← betree.List.partition_at_pivot betree.Message content i0
     let (msgs_left, msgs_right) := p
     let len_left ← betree.List.len (U64 × betree.Message) msgs_left
-    if len_left >= params.betree_params_min_flush_size
+    if len_left >= params.min_flush_size
     then
       do
         let (st0, _) ←
@@ -880,7 +863,7 @@ divergent def betree.Internal.flush_back
         let (n1, node_id_cnt0) ←
           betree.Node.apply_messages_back n params node_id_cnt msgs_left st
         let len_right ← betree.List.len (U64 × betree.Message) msgs_right
-        if len_right >= params.betree_params_min_flush_size
+        if len_right >= params.min_flush_size
         then
           do
             let (n2, node_id_cnt1) ←
@@ -936,18 +919,11 @@ def betree.BeTree.new
     let node_id_cnt0 ← betree.NodeIdCounter.fresh_id_back node_id_cnt
     Result.ret (st0,
       {
-        betree_be_tree_params :=
-          {
-            betree_params_min_flush_size := min_flush_size,
-            betree_params_split_size := split_size
-          },
-        betree_be_tree_node_id_cnt := node_id_cnt0,
-        betree_be_tree_root :=
-          (betree.Node.Leaf
-            {
-              betree_leaf_id := id,
-              betree_leaf_size := (U64.ofInt 0 (by intlit))
-            })
+        params :=
+          { min_flush_size := min_flush_size, split_size := split_size },
+        node_id_cnt := node_id_cnt0,
+        root :=
+          (betree.Node.Leaf { id := id, size := (U64.ofInt 0 (by intlit)) })
       })
 
 /- [betree_main::betree::BeTree::{6}::apply]: forward function -/
@@ -957,11 +933,9 @@ def betree.BeTree.apply
   :=
   do
     let (st0, _) ←
-      betree.Node.apply self.betree_be_tree_root self.betree_be_tree_params
-        self.betree_be_tree_node_id_cnt key msg st
+      betree.Node.apply self.root self.params self.node_id_cnt key msg st
     let _ ←
-      betree.Node.apply_back self.betree_be_tree_root
-        self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
+      betree.Node.apply_back self.root self.params self.node_id_cnt key msg st
     Result.ret (st0, ())
 
 /- [betree_main::betree::BeTree::{6}::apply]: backward function 0 -/
@@ -971,10 +945,8 @@ def betree.BeTree.apply_back
   :=
   do
     let (n, nic) ←
-      betree.Node.apply_back self.betree_be_tree_root
-        self.betree_be_tree_params self.betree_be_tree_node_id_cnt key msg st
-    Result.ret
-      { self with betree_be_tree_node_id_cnt := nic, betree_be_tree_root := n }
+      betree.Node.apply_back self.root self.params self.node_id_cnt key msg st
+    Result.ret { self with node_id_cnt := nic, root := n }
 
 /- [betree_main::betree::BeTree::{6}::insert]: forward function -/
 def betree.BeTree.insert
@@ -1033,14 +1005,14 @@ def betree.BeTree.lookup
   (self : betree.BeTree) (key : U64) (st : State) :
   Result (State × (Option U64))
   :=
-  betree.Node.lookup self.betree_be_tree_root key st
+  betree.Node.lookup self.root key st
 
 /- [betree_main::betree::BeTree::{6}::lookup]: backward function 0 -/
 def betree.BeTree.lookup_back
   (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree :=
   do
-    let n ← betree.Node.lookup_back self.betree_be_tree_root key st
-    Result.ret { self with betree_be_tree_root := n }
+    let n ← betree.Node.lookup_back self.root key st
+    Result.ret { self with root := n }
 
 /- [betree_main::main]: forward function -/
 def main : Result Unit :=
diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index afbdac9a..783ade64 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -22,8 +22,8 @@ inductive betree.Message :=
 
 /- [betree_main::betree::Leaf] -/
 structure betree.Leaf where
-  betree_leaf_id : U64
-  betree_leaf_size : U64
+  id : U64
+  size : U64
 
 mutual
 
@@ -40,18 +40,18 @@ end
 
 /- [betree_main::betree::Params] -/
 structure betree.Params where
-  betree_params_min_flush_size : U64
-  betree_params_split_size : U64
+  min_flush_size : U64
+  split_size : U64
 
 /- [betree_main::betree::NodeIdCounter] -/
 structure betree.NodeIdCounter where
-  betree_node_id_counter_next_node_id : U64
+  next_node_id : U64
 
 /- [betree_main::betree::BeTree] -/
 structure betree.BeTree where
-  betree_be_tree_params : betree.Params
-  betree_be_tree_node_id_cnt : betree.NodeIdCounter
-  betree_be_tree_root : betree.Node
+  params : betree.Params
+  node_id_cnt : betree.NodeIdCounter
+  root : betree.Node
 
 /- The state type used in the state-error monad -/
 axiom State : Type
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index f37c9204..8f22bfba 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -35,12 +35,12 @@ def mk_pair0 (x : U32) (y : U32) : Result (U32 × U32) :=
 
 /- [constants::Pair] -/
 structure Pair (T1 T2 : Type) where
-  pair_x : T1
-  pair_y : T2
+  x : T1
+  y : T2
 
 /- [constants::mk_pair1]: forward function -/
 def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) :=
-  Result.ret { pair_x := x, pair_y := y }
+  Result.ret { x := x, y := y }
 
 /- [constants::P0] -/
 def p0_body : Result (U32 × U32) :=
@@ -59,17 +59,16 @@ def p2_c : (U32 × U32) := eval_global p2_body (by simp)
 
 /- [constants::P3] -/
 def p3_body : Result (Pair U32 U32) :=
-  Result.ret
-  { pair_x := (U32.ofInt 0 (by intlit)), pair_y := (U32.ofInt 1 (by intlit)) }
+  Result.ret { x := (U32.ofInt 0 (by intlit)), y := (U32.ofInt 1 (by intlit)) }
 def p3_c : Pair U32 U32 := eval_global p3_body (by simp)
 
 /- [constants::Wrap] -/
 structure Wrap (T : Type) where
-  wrap_val : T
+  val : T
 
 /- [constants::Wrap::{0}::new]: forward function -/
 def Wrap.new (T : Type) (val : T) : Result (Wrap T) :=
-  Result.ret { wrap_val := val }
+  Result.ret { val := val }
 
 /- [constants::Y] -/
 def y_body : Result (Wrap I32) := Wrap.new I32 (I32.ofInt 2 (by intlit))
@@ -77,7 +76,7 @@ def y_c : Wrap I32 := eval_global y_body (by simp)
 
 /- [constants::unwrap_y]: forward function -/
 def unwrap_y : Result I32 :=
-  Result.ret y_c.wrap_val
+  Result.ret y_c.val
 
 /- [constants::YVAL] -/
 def yval_body : Result I32 := unwrap_y
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 34ff1379..5e11ffdd 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -38,10 +38,10 @@ def HashMap.new_with_capacity
     let i0 ← i / max_load_divisor
     Result.ret
       {
-        hash_map_num_entries := (Usize.ofInt 0 (by intlit)),
-        hash_map_max_load_factor := (max_load_dividend, max_load_divisor),
-        hash_map_max_load := i0,
-        hash_map_slots := slots
+        num_entries := (Usize.ofInt 0 (by intlit)),
+        max_load_factor := (max_load_dividend, max_load_divisor),
+        max_load := i0,
+        slots := slots
       }
 
 /- [hashmap::HashMap::{0}::new]: forward function -/
@@ -66,19 +66,13 @@ divergent def HashMap.clear_loop
    (there is a single backward function, and the forward function returns ()) -/
 def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) :=
   do
-    let v ←
-      HashMap.clear_loop T self.hash_map_slots (Usize.ofInt 0 (by intlit))
+    let v ← HashMap.clear_loop T self.slots (Usize.ofInt 0 (by intlit))
     Result.ret
-      {
-        self
-          with
-          hash_map_num_entries := (Usize.ofInt 0 (by intlit)),
-          hash_map_slots := v
-      }
+      { self with num_entries := (Usize.ofInt 0 (by intlit)), slots := v }
 
 /- [hashmap::HashMap::{0}::len]: forward function -/
 def HashMap.len (T : Type) (self : HashMap T) : Result Usize :=
-  Result.ret self.hash_map_num_entries
+  Result.ret self.num_entries
 
 /- [hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function -/
 divergent def HashMap.insert_in_list_loop
@@ -122,23 +116,22 @@ def HashMap.insert_no_resize
   :=
   do
     let hash ← hash_key key
-    let i := Vec.len (List T) self.hash_map_slots
+    let i := Vec.len (List T) self.slots
     let hash_mod ← hash % i
-    let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod
+    let l ← Vec.index_mut (List T) self.slots hash_mod
     let inserted ← HashMap.insert_in_list T key value l
     if inserted
     then
       do
-        let i0 ← self.hash_map_num_entries + (Usize.ofInt 1 (by intlit))
+        let i0 ← self.num_entries + (Usize.ofInt 1 (by intlit))
         let l0 ← HashMap.insert_in_list_back T key value l
-        let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0
-        Result.ret
-          { self with hash_map_num_entries := i0, hash_map_slots := v }
+        let v ← Vec.index_mut_back (List T) self.slots hash_mod l0
+        Result.ret { self with num_entries := i0, slots := v }
     else
       do
         let l0 ← HashMap.insert_in_list_back T key value l
-        let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0
-        Result.ret { self with hash_map_slots := v }
+        let v ← Vec.index_mut_back (List T) self.slots hash_mod l0
+        Result.ret { self with slots := v }
 
 /- [core::num::u32::{9}::MAX] -/
 def core_num_u32_max_body : Result U32 :=
@@ -194,9 +187,9 @@ def HashMap.move_elements
 def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
   do
     let max_usize ← Scalar.cast .Usize core_num_u32_max_c
-    let capacity := Vec.len (List T) self.hash_map_slots
+    let capacity := Vec.len (List T) self.slots
     let n1 ← max_usize / (Usize.ofInt 2 (by intlit))
-    let (i, i0) := self.hash_map_max_load_factor
+    let (i, i0) := self.max_load_factor
     let i1 ← n1 / i
     if capacity <= i1
     then
@@ -204,16 +197,14 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
         let i2 ← capacity * (Usize.ofInt 2 (by intlit))
         let ntable ← HashMap.new_with_capacity T i2 i i0
         let (ntable0, _) ←
-          HashMap.move_elements T ntable self.hash_map_slots
-            (Usize.ofInt 0 (by intlit))
+          HashMap.move_elements T ntable self.slots (Usize.ofInt 0 (by intlit))
         Result.ret
           {
             ntable0
               with
-              hash_map_num_entries := self.hash_map_num_entries,
-              hash_map_max_load_factor := (i, i0)
+              num_entries := self.num_entries, max_load_factor := (i, i0)
           }
-    else Result.ret { self with hash_map_max_load_factor := (i, i0) }
+    else Result.ret { self with max_load_factor := (i, i0) }
 
 /- [hashmap::HashMap::{0}::insert]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
@@ -224,7 +215,7 @@ def HashMap.insert
   do
     let self0 ← HashMap.insert_no_resize T self key value
     let i ← HashMap.len T self0
-    if i > self0.hash_map_max_load
+    if i > self0.max_load
     then HashMap.try_resize T self0
     else Result.ret self0
 
@@ -248,9 +239,9 @@ def HashMap.contains_key
   (T : Type) (self : HashMap T) (key : Usize) : Result Bool :=
   do
     let hash ← hash_key key
-    let i := Vec.len (List T) self.hash_map_slots
+    let i := Vec.len (List T) self.slots
     let hash_mod ← hash % i
-    let l ← Vec.index (List T) self.hash_map_slots hash_mod
+    let l ← Vec.index (List T) self.slots hash_mod
     HashMap.contains_key_in_list T key l
 
 /- [hashmap::HashMap::{0}::get_in_list]: loop 0: forward function -/
@@ -271,9 +262,9 @@ def HashMap.get_in_list (T : Type) (key : Usize) (ls : List T) : Result T :=
 def HashMap.get (T : Type) (self : HashMap T) (key : Usize) : Result T :=
   do
     let hash ← hash_key key
-    let i := Vec.len (List T) self.hash_map_slots
+    let i := Vec.len (List T) self.slots
     let hash_mod ← hash % i
-    let l ← Vec.index (List T) self.hash_map_slots hash_mod
+    let l ← Vec.index (List T) self.slots hash_mod
     HashMap.get_in_list T key l
 
 /- [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function -/
@@ -313,9 +304,9 @@ def HashMap.get_mut_in_list_back
 def HashMap.get_mut (T : Type) (self : HashMap T) (key : Usize) : Result T :=
   do
     let hash ← hash_key key
-    let i := Vec.len (List T) self.hash_map_slots
+    let i := Vec.len (List T) self.slots
     let hash_mod ← hash % i
-    let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod
+    let l ← Vec.index_mut (List T) self.slots hash_mod
     HashMap.get_mut_in_list T l key
 
 /- [hashmap::HashMap::{0}::get_mut]: backward function 0 -/
@@ -325,12 +316,12 @@ def HashMap.get_mut_back
   :=
   do
     let hash ← hash_key key
-    let i := Vec.len (List T) self.hash_map_slots
+    let i := Vec.len (List T) self.slots
     let hash_mod ← hash % i
-    let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod
+    let l ← Vec.index_mut (List T) self.slots hash_mod
     let l0 ← HashMap.get_mut_in_list_back T l key ret0
-    let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0
-    Result.ret { self with hash_map_slots := v }
+    let v ← Vec.index_mut_back (List T) self.slots hash_mod l0
+    Result.ret { self with slots := v }
 
 /- [hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function -/
 divergent def HashMap.remove_from_list_loop
@@ -378,15 +369,15 @@ def HashMap.remove
   (T : Type) (self : HashMap T) (key : Usize) : Result (Option T) :=
   do
     let hash ← hash_key key
-    let i := Vec.len (List T) self.hash_map_slots
+    let i := Vec.len (List T) self.slots
     let hash_mod ← hash % i
-    let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod
+    let l ← Vec.index_mut (List T) self.slots hash_mod
     let x ← HashMap.remove_from_list T key l
     match x with
     | Option.none => Result.ret Option.none
     | Option.some x0 =>
       do
-        let _ ← self.hash_map_num_entries - (Usize.ofInt 1 (by intlit))
+        let _ ← self.num_entries - (Usize.ofInt 1 (by intlit))
         Result.ret (Option.some x0)
 
 /- [hashmap::HashMap::{0}::remove]: backward function 0 -/
@@ -394,23 +385,22 @@ def HashMap.remove_back
   (T : Type) (self : HashMap T) (key : Usize) : Result (HashMap T) :=
   do
     let hash ← hash_key key
-    let i := Vec.len (List T) self.hash_map_slots
+    let i := Vec.len (List T) self.slots
     let hash_mod ← hash % i
-    let l ← Vec.index_mut (List T) self.hash_map_slots hash_mod
+    let l ← Vec.index_mut (List T) self.slots hash_mod
     let x ← HashMap.remove_from_list T key l
     match x with
     | Option.none =>
       do
         let l0 ← HashMap.remove_from_list_back T key l
-        let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0
-        Result.ret { self with hash_map_slots := v }
+        let v ← Vec.index_mut_back (List T) self.slots hash_mod l0
+        Result.ret { self with slots := v }
     | Option.some x0 =>
       do
-        let i0 ← self.hash_map_num_entries - (Usize.ofInt 1 (by intlit))
+        let i0 ← self.num_entries - (Usize.ofInt 1 (by intlit))
         let l0 ← HashMap.remove_from_list_back T key l
-        let v ← Vec.index_mut_back (List T) self.hash_map_slots hash_mod l0
-        Result.ret
-          { self with hash_map_num_entries := i0, hash_map_slots := v }
+        let v ← Vec.index_mut_back (List T) self.slots hash_mod l0
+        Result.ret { self with num_entries := i0, slots := v }
 
 /- [hashmap::test1]: forward function -/
 def test1 : Result Unit :=
diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean
index 7530f3b9..6606cf9e 100644
--- a/tests/lean/Hashmap/Types.lean
+++ b/tests/lean/Hashmap/Types.lean
@@ -11,9 +11,9 @@ inductive List (T : Type) :=
 
 /- [hashmap::HashMap] -/
 structure HashMap (T : Type) where
-  hash_map_num_entries : Usize
-  hash_map_max_load_factor : (Usize × Usize)
-  hash_map_max_load : Usize
-  hash_map_slots : Vec (List T)
+  num_entries : Usize
+  max_load_factor : (Usize × Usize)
+  max_load : Usize
+  slots : Vec (List T)
 
 end hashmap
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index b1afcd44..e82cc9b2 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -43,11 +43,10 @@ def hashmap.HashMap.new_with_capacity
     let i0 ← i / max_load_divisor
     Result.ret
       {
-        hashmap_hash_map_num_entries := (Usize.ofInt 0 (by intlit)),
-        hashmap_hash_map_max_load_factor :=
-          (max_load_dividend, max_load_divisor),
-        hashmap_hash_map_max_load := i0,
-        hashmap_hash_map_slots := slots
+        num_entries := (Usize.ofInt 0 (by intlit)),
+        max_load_factor := (max_load_dividend, max_load_divisor),
+        max_load := i0,
+        slots := slots
       }
 
 /- [hashmap_main::hashmap::HashMap::{0}::new]: forward function -/
@@ -77,19 +76,13 @@ def hashmap.HashMap.clear
   (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
   do
     let v ←
-      hashmap.HashMap.clear_loop T self.hashmap_hash_map_slots
-        (Usize.ofInt 0 (by intlit))
+      hashmap.HashMap.clear_loop T self.slots (Usize.ofInt 0 (by intlit))
     Result.ret
-      {
-        self
-          with
-          hashmap_hash_map_num_entries := (Usize.ofInt 0 (by intlit)),
-          hashmap_hash_map_slots := v
-      }
+      { self with num_entries := (Usize.ofInt 0 (by intlit)), slots := v }
 
 /- [hashmap_main::hashmap::HashMap::{0}::len]: forward function -/
 def hashmap.HashMap.len (T : Type) (self : hashmap.HashMap T) : Result Usize :=
-  Result.ret self.hashmap_hash_map_num_entries
+  Result.ret self.num_entries
 
 /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list]: loop 0: forward function -/
 divergent def hashmap.HashMap.insert_in_list_loop
@@ -138,33 +131,22 @@ def hashmap.HashMap.insert_no_resize
   :=
   do
     let hash ← hashmap.hash_key key
-    let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots
+    let i := Vec.len (hashmap.List T) self.slots
     let hash_mod ← hash % i
-    let l ←
-      Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod
+    let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod
     let inserted ← hashmap.HashMap.insert_in_list T key value l
     if inserted
     then
       do
-        let i0 ← self.hashmap_hash_map_num_entries +
-          (Usize.ofInt 1 (by intlit))
+        let i0 ← self.num_entries + (Usize.ofInt 1 (by intlit))
         let l0 ← hashmap.HashMap.insert_in_list_back T key value l
-        let v ←
-          Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots
-            hash_mod l0
-        Result.ret
-          {
-            self
-              with
-              hashmap_hash_map_num_entries := i0, hashmap_hash_map_slots := v
-          }
+        let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0
+        Result.ret { self with num_entries := i0, slots := v }
     else
       do
         let l0 ← hashmap.HashMap.insert_in_list_back T key value l
-        let v ←
-          Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots
-            hash_mod l0
-        Result.ret { self with hashmap_hash_map_slots := v }
+        let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0
+        Result.ret { self with slots := v }
 
 /- [core::num::u32::{9}::MAX] -/
 def core_num_u32_max_body : Result U32 :=
@@ -227,9 +209,9 @@ def hashmap.HashMap.try_resize
   (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
   do
     let max_usize ← Scalar.cast .Usize core_num_u32_max_c
-    let capacity := Vec.len (hashmap.List T) self.hashmap_hash_map_slots
+    let capacity := Vec.len (hashmap.List T) self.slots
     let n1 ← max_usize / (Usize.ofInt 2 (by intlit))
-    let (i, i0) := self.hashmap_hash_map_max_load_factor
+    let (i, i0) := self.max_load_factor
     let i1 ← n1 / i
     if capacity <= i1
     then
@@ -237,16 +219,15 @@ def hashmap.HashMap.try_resize
         let i2 ← capacity * (Usize.ofInt 2 (by intlit))
         let ntable ← hashmap.HashMap.new_with_capacity T i2 i i0
         let (ntable0, _) ←
-          hashmap.HashMap.move_elements T ntable self.hashmap_hash_map_slots
+          hashmap.HashMap.move_elements T ntable self.slots
             (Usize.ofInt 0 (by intlit))
         Result.ret
           {
             ntable0
               with
-              hashmap_hash_map_num_entries := self.hashmap_hash_map_num_entries,
-              hashmap_hash_map_max_load_factor := (i, i0)
+              num_entries := self.num_entries, max_load_factor := (i, i0)
           }
-    else Result.ret { self with hashmap_hash_map_max_load_factor := (i, i0) }
+    else Result.ret { self with max_load_factor := (i, i0) }
 
 /- [hashmap_main::hashmap::HashMap::{0}::insert]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
@@ -257,7 +238,7 @@ def hashmap.HashMap.insert
   do
     let self0 ← hashmap.HashMap.insert_no_resize T self key value
     let i ← hashmap.HashMap.len T self0
-    if i > self0.hashmap_hash_map_max_load
+    if i > self0.max_load
     then hashmap.HashMap.try_resize T self0
     else Result.ret self0
 
@@ -281,9 +262,9 @@ def hashmap.HashMap.contains_key
   (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result Bool :=
   do
     let hash ← hashmap.hash_key key
-    let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots
+    let i := Vec.len (hashmap.List T) self.slots
     let hash_mod ← hash % i
-    let l ← Vec.index (hashmap.List T) self.hashmap_hash_map_slots hash_mod
+    let l ← Vec.index (hashmap.List T) self.slots hash_mod
     hashmap.HashMap.contains_key_in_list T key l
 
 /- [hashmap_main::hashmap::HashMap::{0}::get_in_list]: loop 0: forward function -/
@@ -306,9 +287,9 @@ def hashmap.HashMap.get
   (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T :=
   do
     let hash ← hashmap.hash_key key
-    let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots
+    let i := Vec.len (hashmap.List T) self.slots
     let hash_mod ← hash % i
-    let l ← Vec.index (hashmap.List T) self.hashmap_hash_map_slots hash_mod
+    let l ← Vec.index (hashmap.List T) self.slots hash_mod
     hashmap.HashMap.get_in_list T key l
 
 /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function -/
@@ -353,10 +334,9 @@ def hashmap.HashMap.get_mut
   (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T :=
   do
     let hash ← hashmap.hash_key key
-    let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots
+    let i := Vec.len (hashmap.List T) self.slots
     let hash_mod ← hash % i
-    let l ←
-      Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod
+    let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod
     hashmap.HashMap.get_mut_in_list T l key
 
 /- [hashmap_main::hashmap::HashMap::{0}::get_mut]: backward function 0 -/
@@ -366,15 +346,12 @@ def hashmap.HashMap.get_mut_back
   :=
   do
     let hash ← hashmap.hash_key key
-    let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots
+    let i := Vec.len (hashmap.List T) self.slots
     let hash_mod ← hash % i
-    let l ←
-      Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod
+    let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod
     let l0 ← hashmap.HashMap.get_mut_in_list_back T l key ret0
-    let v ←
-      Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots hash_mod
-        l0
-    Result.ret { self with hashmap_hash_map_slots := v }
+    let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0
+    Result.ret { self with slots := v }
 
 /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list]: loop 0: forward function -/
 divergent def hashmap.HashMap.remove_from_list_loop
@@ -426,17 +403,15 @@ def hashmap.HashMap.remove
   (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result (Option T) :=
   do
     let hash ← hashmap.hash_key key
-    let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots
+    let i := Vec.len (hashmap.List T) self.slots
     let hash_mod ← hash % i
-    let l ←
-      Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod
+    let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod
     let x ← hashmap.HashMap.remove_from_list T key l
     match x with
     | Option.none => Result.ret Option.none
     | Option.some x0 =>
       do
-        let _ ← self.hashmap_hash_map_num_entries -
-          (Usize.ofInt 1 (by intlit))
+        let _ ← self.num_entries - (Usize.ofInt 1 (by intlit))
         Result.ret (Option.some x0)
 
 /- [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 -/
@@ -446,33 +421,22 @@ def hashmap.HashMap.remove_back
   :=
   do
     let hash ← hashmap.hash_key key
-    let i := Vec.len (hashmap.List T) self.hashmap_hash_map_slots
+    let i := Vec.len (hashmap.List T) self.slots
     let hash_mod ← hash % i
-    let l ←
-      Vec.index_mut (hashmap.List T) self.hashmap_hash_map_slots hash_mod
+    let l ← Vec.index_mut (hashmap.List T) self.slots hash_mod
     let x ← hashmap.HashMap.remove_from_list T key l
     match x with
     | Option.none =>
       do
         let l0 ← hashmap.HashMap.remove_from_list_back T key l
-        let v ←
-          Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots
-            hash_mod l0
-        Result.ret { self with hashmap_hash_map_slots := v }
+        let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0
+        Result.ret { self with slots := v }
     | Option.some x0 =>
       do
-        let i0 ← self.hashmap_hash_map_num_entries -
-          (Usize.ofInt 1 (by intlit))
+        let i0 ← self.num_entries - (Usize.ofInt 1 (by intlit))
         let l0 ← hashmap.HashMap.remove_from_list_back T key l
-        let v ←
-          Vec.index_mut_back (hashmap.List T) self.hashmap_hash_map_slots
-            hash_mod l0
-        Result.ret
-          {
-            self
-              with
-              hashmap_hash_map_num_entries := i0, hashmap_hash_map_slots := v
-          }
+        let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0
+        Result.ret { self with num_entries := i0, slots := v }
 
 /- [hashmap_main::hashmap::test1]: forward function -/
 def hashmap.test1 : Result Unit :=
diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean
index ac195e3d..3b3d0d7c 100644
--- a/tests/lean/HashmapMain/Types.lean
+++ b/tests/lean/HashmapMain/Types.lean
@@ -11,10 +11,10 @@ inductive hashmap.List (T : Type) :=
 
 /- [hashmap_main::hashmap::HashMap] -/
 structure hashmap.HashMap (T : Type) where
-  hashmap_hash_map_num_entries : Usize
-  hashmap_hash_map_max_load_factor : (Usize × Usize)
-  hashmap_hash_map_max_load : Usize
-  hashmap_hash_map_slots : Vec (hashmap.List T)
+  num_entries : Usize
+  max_load_factor : (Usize × Usize)
+  max_load : Usize
+  slots : Vec (hashmap.List T)
 
 /- The state type used in the state-error monad -/
 axiom State : Type
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index dc744a29..1c6421bb 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -6,8 +6,8 @@ namespace no_nested_borrows
 
 /- [no_nested_borrows::Pair] -/
 structure Pair (T1 T2 : Type) where
-  pair_x : T1
-  pair_y : T2
+  x : T1
+  y : T2
 
 /- [no_nested_borrows::List] -/
 inductive List (T : Type) :=
@@ -431,71 +431,52 @@ def id_mut_pair4_back'b
 
 /- [no_nested_borrows::StructWithTuple] -/
 structure StructWithTuple (T1 T2 : Type) where
-  struct_with_tuple_p : (T1 × T2)
+  p : (T1 × T2)
 
 /- [no_nested_borrows::new_tuple1]: forward function -/
 def new_tuple1 : Result (StructWithTuple U32 U32) :=
-  Result.ret
-  {
-    struct_with_tuple_p :=
-      ((U32.ofInt 1 (by intlit)), (U32.ofInt 2 (by intlit)))
-  }
+  Result.ret { p := ((U32.ofInt 1 (by intlit)), (U32.ofInt 2 (by intlit))) }
 
 /- [no_nested_borrows::new_tuple2]: forward function -/
 def new_tuple2 : Result (StructWithTuple I16 I16) :=
-  Result.ret
-  {
-    struct_with_tuple_p :=
-      ((I16.ofInt 1 (by intlit)), (I16.ofInt 2 (by intlit)))
-  }
+  Result.ret { p := ((I16.ofInt 1 (by intlit)), (I16.ofInt 2 (by intlit))) }
 
 /- [no_nested_borrows::new_tuple3]: forward function -/
 def new_tuple3 : Result (StructWithTuple U64 I64) :=
-  Result.ret
-  {
-    struct_with_tuple_p :=
-      ((U64.ofInt 1 (by intlit)), (I64.ofInt 2 (by intlit)))
-  }
+  Result.ret { p := ((U64.ofInt 1 (by intlit)), (I64.ofInt 2 (by intlit))) }
 
 /- [no_nested_borrows::StructWithPair] -/
 structure StructWithPair (T1 T2 : Type) where
-  struct_with_pair_p : Pair T1 T2
+  p : Pair T1 T2
 
 /- [no_nested_borrows::new_pair1]: forward function -/
 def new_pair1 : Result (StructWithPair U32 U32) :=
   Result.ret
-  {
-    struct_with_pair_p :=
-      {
-        pair_x := (U32.ofInt 1 (by intlit)),
-        pair_y := (U32.ofInt 2 (by intlit))
-      }
-  }
+  { p := { x := (U32.ofInt 1 (by intlit)), y := (U32.ofInt 2 (by intlit)) } }
 
 /- [no_nested_borrows::test_constants]: forward function -/
 def test_constants : Result Unit :=
   do
     let swt ← new_tuple1
-    let (i, _) := swt.struct_with_tuple_p
+    let (i, _) := swt.p
     if not (i = (U32.ofInt 1 (by intlit)))
     then Result.fail Error.panic
     else
       do
         let swt0 ← new_tuple2
-        let (i0, _) := swt0.struct_with_tuple_p
+        let (i0, _) := swt0.p
         if not (i0 = (I16.ofInt 1 (by intlit)))
         then Result.fail Error.panic
         else
           do
             let swt1 ← new_tuple3
-            let (i1, _) := swt1.struct_with_tuple_p
+            let (i1, _) := swt1.p
             if not (i1 = (U64.ofInt 1 (by intlit)))
             then Result.fail Error.panic
             else
               do
                 let swp ← new_pair1
-                if not (swp.struct_with_pair_p.pair_x =
-                  (U32.ofInt 1 (by intlit)))
+                if not (swp.p.x = (U32.ofInt 1 (by intlit)))
                 then Result.fail Error.panic
                 else Result.ret ()