From 8f27b1e64ef3dab9a314df4794ae8c361a8ef3dd Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Wed, 25 Jan 2023 20:46:54 -0800
Subject: Fixup one primitive that is not assumed to be monadic

---
 backends/lean/primitives.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'backends')

diff --git a/backends/lean/primitives.lean b/backends/lean/primitives.lean
index d1d04285..3b1d39fc 100644
--- a/backends/lean/primitives.lean
+++ b/backends/lean/primitives.lean
@@ -133,7 +133,7 @@ macro_rules
 
 def vec (α : Type u) := { l : List α // List.length l < USize.size }
 
-def vec_new (α : Type u): result (vec α) := return ⟨ [], by {
+def vec_new (α : Type u): vec α := ⟨ [], by {
   match USize.size, usize_size_eq with
   | _, Or.inl rfl => simp
   | _, Or.inr rfl => simp
@@ -145,8 +145,7 @@ def vec_len (α : Type u) (v : vec α) : USize :=
   let ⟨ v, l ⟩ := v
   USize.ofNatCore (List.length v) l
 
-#eval do
-  return (vec_len Nat (<- vec_new Nat))
+#eval vec_len Nat (vec_new Nat)
  
 def vec_push_fwd (α : Type u) (_ : vec α) (_ : α) : Unit := ()
 
@@ -172,7 +171,8 @@ def vec_push_back (α : Type u) (v : vec α) (x : α) : { res: result (vec α) /
   -- select the `val` field if the context provides a type annotation. We
   -- annotate `x`, which relieves us of having to write `.val` on the right-hand
   -- side of the monadic let.
-  let x: vec Nat ← vec_push_back Nat (<- vec_new Nat) 1
+  let v := vec_new Nat
+  let x: vec Nat ← (vec_push_back Nat v 1: result (vec Nat)) -- WHY do we need the type annotation here?
   -- TODO: strengthen post-condition above and do a demo to show that we can
   -- safely eliminate the `fail` case
   return (vec_len Nat x)
-- 
cgit v1.2.3