Idris2/tests/idris2/perror007/expected

1/1: Building StrError1 (StrError1.idr)
Error: Expected 'case', 'if', 'do', application or operator expression.

StrError1.idr:2:24--2:25
 1 | foo : String
 2 | foo = "empty interp: \{}"
                            ^

1/1: Building StrError2 (StrError2.idr)
Error: Expected 'case', 'if', 'do', application or operator expression.

StrError2.idr:2:19--2:20
 1 | foo : String
 2 | foo = "nested: \{ " \{ 1 +  } " }"
                       ^

1/1: Building StrError3 (StrError3.idr)
Error: Expected 'case', 'if', 'do', application or operator expression.

StrError3.idr:2:7--2:8
 1 | foo : String
 2 | foo = "incomplete: \{ a <+> }"
           ^

1/1: Building StrError4 (StrError4.idr)
Error: Bracket is not properly closed.

StrError4.idr:2:7--2:8
 1 | foo : String
 2 | foo = """"""
           ^

1/1: Building StrError5 (StrError5.idr)
Error: While processing multi-line string. Indentation not enough.

StrError5.idr:3:1--4:5
 3 |    a
 4 |     """

1/1: Building StrError6 (StrError6.idr)
Error: Bracket is not properly closed.

StrError6.idr:2:7--2:8
 1 | foo : String
 2 | foo = """a
           ^

1/1: Building StrError7 (StrError7.idr)
Error: Bracket is not properly closed.

StrError7.idr:2:7--2:8
 1 | foo : String
 2 | foo = """a"""
           ^

1/1: Building StrError8 (StrError8.idr)
Error: Bracket is not properly closed.

StrError8.idr:2:7--2:8
 1 | foo : String
 2 | foo = """\{"hello"}
           ^

1/1: Building StrError9 (StrError9.idr)
Error: While processing multi-line string. Unexpected interpolation in the last line.

StrError9.idr:3:1--3:11
 1 | foo : String
 2 | foo = """
 3 | \{"hello"}"""
     ^^^^^^^^^^

1/1: Building StrError10 (StrError10.idr)
Error: While processing multi-line string. Unexpected character in the last line.

StrError10.idr:3:1--3:2
 1 | foo : String
 2 | foo = """
 3 | a"""
     ^

1/1: Building StrError11 (StrError11.idr)
Error: Multi-line string is expected to begin with """.

StrError11.idr:4:1--4:2
 1 | foo : String
 2 | foo = "a
 3 |     "
     ^

1/1: Building StrError12 (StrError12.idr)
Error: While processing multi-line string. Indentation not enough.

StrError12.idr:3:1--3:3
 1 | foo : String
 2 | foo = """
 3 |   \{show 1}
     ^^