From 5ca36bfc50083a01af2b7ae5f75993a520757ef5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jul 2023 15:17:58 +0200
Subject: Simplify the names used in Primitives.lean

---
 tests/lean/BetreeMain/Funs.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tests/lean/BetreeMain')

diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 3a678c71..074fff5e 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -124,13 +124,13 @@ divergent def betree.List.split_at_fwd
 /- [betree_main::betree::List::{1}::push_front] -/
 def betree.List.push_front_fwd_back
   (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) :=
-  let tl := mem_replace_fwd (betree.List T) self betree.List.Nil
+  let tl := mem.replace_fwd (betree.List T) self betree.List.Nil
   let l := tl
   Result.ret (betree.List.Cons x l)
 
 /- [betree_main::betree::List::{1}::pop_front] -/
 def betree.List.pop_front_fwd (T : Type) (self : betree.List T) : Result T :=
-  let ls := mem_replace_fwd (betree.List T) self betree.List.Nil
+  let ls := mem.replace_fwd (betree.List T) self betree.List.Nil
   match ls with
   | betree.List.Cons x tl => Result.ret x
   | betree.List.Nil => Result.fail Error.panic
@@ -138,7 +138,7 @@ def betree.List.pop_front_fwd (T : Type) (self : betree.List T) : Result T :=
 /- [betree_main::betree::List::{1}::pop_front] -/
 def betree.List.pop_front_back
   (T : Type) (self : betree.List T) : Result (betree.List T) :=
-  let ls := mem_replace_fwd (betree.List T) self betree.List.Nil
+  let ls := mem.replace_fwd (betree.List T) self betree.List.Nil
   match ls with
   | betree.List.Cons x tl => Result.ret tl
   | betree.List.Nil => Result.fail Error.panic
-- 
cgit v1.2.3