| def foo (x? : Option Nat) : IO Nat := do | |
| let some x := x? | return 0 | |
| IO.println s!"x: {x}" | |
| return x | |
| def testFoo (input : Option Nat) (expected : Nat) : IO Unit := do | |
| assert! (← foo input) == expected | |
| /-- info: x: 10 -/ | |
| #guard_msgs in | |
| #eval testFoo (some 10) 10 | |
| #guard_msgs in | |
| #eval testFoo none 0 | |
| /-- info: x: 1 -/ | |
| #guard_msgs in | |
| #eval testFoo (some 1) 1 | |
| /-- info: "ok" -/ | |
| #guard_msgs in | |
| #eval Id.run do | |
| let mut x := 0 | |
| let y <- do | |
| let true := false | do x := x + 3; pure 0 -- NB: this returns from the inner `do` block | |
| x := x + 100 | |
| return "unreachable" | |
| if x + y < 23 then pure "ok" else pure "wrong" | |
| -- doLetElse syntax and match syntax used to refine the result type of the do block. | |
| -- In the interest of efficient elaboration, the new do elabarotor abandoned the functionality. | |
| -- Users are expected to use term `match` where needed. | |
| /-- | |
| error: Type mismatch | |
| y | |
| has type | |
| Fin 3 | |
| but is expected to have type | |
| Fin (x + 1) | |
| -/ | |
| #guard_msgs in | |
| def bar (x : Nat) : IO (Fin (x + 1)) := do | |
| let 2 := x | return 0 | |
| let y : Fin 3 := ⟨1, by decide⟩ | |
| return y |