lean4-htt/tests/lean/letArrowOutsideDo.lean

3 lines
63 B
Text

def myFun (n : Nat) : IO Nat :=
let q ← (10 : Nat)
n + q