diff options
| author | Son Ho | 2023-07-05 15:17:58 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-05 15:17:58 +0200 |
| commit | 5ca36bfc50083a01af2b7ae5f75993a520757ef5 (patch) | |
| tree | 11660b73a27ad2e0807a18ac9286a1e87c560050 /tests/lean/BetreeMain | |
| parent | c07721dedb2cfe4c726c42606e623395cdfe5b80 (diff) | |
Simplify the names used in Primitives.lean
Diffstat (limited to 'tests/lean/BetreeMain')
| -rw-r--r-- | tests/lean/BetreeMain/Funs.lean | 6 |
1 files changed, 3 insertions, 3 deletions
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 |