test: do with optional ;
This commit is contained in:
parent
96a0fb41be
commit
765a8ac984
1 changed files with 17 additions and 0 deletions
17
tests/lean/run/doNotation2.lean
Normal file
17
tests/lean/run/doNotation2.lean
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
new_frontend
|
||||
|
||||
def f (x : Nat) : IO Nat := do
|
||||
IO.println "hello world"
|
||||
let aux (y : Nat) (z : Nat) : IO Nat := do
|
||||
IO.println "aux started"
|
||||
IO.println ("y: " ++ toString y ++ ", z: " ++ toString z)
|
||||
return x+y
|
||||
aux x
|
||||
(x + 1) -- It is part of the application since it is indented
|
||||
aux x (x -- parentheses use `withoutPosition`
|
||||
-1)
|
||||
aux x x;
|
||||
aux x
|
||||
x
|
||||
|
||||
#eval f 10
|
||||
Loading…
Add table
Reference in a new issue