diff options
| -rw-r--r-- | backends/lean/primitives.lean | 8 | ||||
| -rw-r--r-- | tests/lean/hashmap_on_disk/Base/Primitives.lean | 8 |
2 files changed, 8 insertions, 8 deletions
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) diff --git a/tests/lean/hashmap_on_disk/Base/Primitives.lean b/tests/lean/hashmap_on_disk/Base/Primitives.lean index d1d04285..3b1d39fc 100644 --- a/tests/lean/hashmap_on_disk/Base/Primitives.lean +++ b/tests/lean/hashmap_on_disk/Base/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) |