e9d85f49e6
Based on the discussion at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/for.2C.20unexpected.20need.20for.20type.20ascription/near/269083574 The consensus seemed to be that "auto pure" is more confusing than its worth.
19 lines
451 B
Text
19 lines
451 B
Text
import Lean
|
|
|
|
open Lean
|
|
|
|
def f (xs : List Nat) (delta : Nat) : List Nat :=
|
|
runST (fun ω => visit xs |>.run)
|
|
where
|
|
visit {ω} : List Nat → MonadCacheT Nat Nat (ST ω) (List Nat)
|
|
| [] => return []
|
|
| a::as => do
|
|
let b ← checkCache a fun _ => return a + delta
|
|
return b :: (← visit as)
|
|
|
|
def tst (xs : List Nat) : IO Unit := do
|
|
IO.println (f xs 10)
|
|
IO.println (f xs 20)
|
|
IO.println (f xs 30)
|
|
|
|
#eval tst [1, 2, 3, 1, 2]
|