From 4828b77847ee981f5c6a1bbad7f8e6ed0e58eb0f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 16:08:32 +0200
Subject: Rename Result.ret as Result.ok in the backends

---
 backends/lean/Base/Primitives/Alloc.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'backends/lean/Base/Primitives/Alloc.lean')

diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean
index 1f470fe1..15fe1ff9 100644
--- a/backends/lean/Base/Primitives/Alloc.lean
+++ b/backends/lean/Base/Primitives/Alloc.lean
@@ -11,8 +11,8 @@ namespace boxed -- alloc.boxed
 
 namespace Box -- alloc.boxed.Box
 
-def deref (T : Type) (x : T) : Result T := ret x
-def deref_mut (T : Type) (x : T) : Result (T × (T → Result T)) := ret (x, λ x => ret x)
+def deref (T : Type) (x : T) : Result T := ok x
+def deref_mut (T : Type) (x : T) : Result (T × (T → Result T)) := ok (x, λ x => ok x)
 
 /-- Trait instance -/
 def coreopsDerefInst (Self : Type) :
-- 
cgit v1.2.3