Idris2/tests/idris2/with004/expected

1/1: Building Issue637 (Issue637.idr)
Main> 11
Main> 
Bye for now!
1/1: Building Issue637-2 (Issue637-2.idr)
Error: Expected an indented non-empty block.

Issue637-2:5:3--5:4
 1 | namespace A
 2 |   export
 3 |   foo3 : Int -> Int
 4 |   foo3 x with (x + 1)
 5 |   foo3 x | y = y + x
       ^

1/1: Building Issue637-3 (Issue637-3.idr)
Error: Expected an indented non-empty block.

Issue637-3:3:1--3:2
 1 | foo5 : Int -> Int
 2 | foo5 x with (x + 1)
 3 | foo5 x | y = y + x
     ^