Idris2/tests/idris2/reg003/expected

1/1: Building Holes (Holes.idr)
Error: While processing type of Vect_ext. Undefined name ~=~. 

Holes.idr:4:64--4:85
   |
 4 | Vect_ext : (v : Vect n a) -> (w : Vect n a) -> ((i : Fin n) -> index i v = index i w)
   |                                                                ^^^^^^^^^^^^^^^^^^^^^

Error: While processing type of Weird. Undefined name ~=~. 

Holes.idr:7:26--7:31
   |
 7 | Weird : (v: Vect n a) -> v = v
   |                          ^^^^^

Error: No type declaration for Main.Weird.

Holes.idr:8:1--8:41
   |
 8 | Weird v =  Vect_ext ?hole0 ?hole1 ?hole2
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Error: While processing type of f. Undefined name Bool. 

Holes.idr:10:5--10:9
    |
 10 | f : Bool -> Nat
    |     ^^^^

Error: No type declaration for Main.f.

Holes.idr:11:1--11:11
    |
 11 | f True = 0
    | ^^^^^^^^^^

Main> Error: Undefined name help. 

(interactive):1:4--1:8
   |
 1 | :t help
   |    ^^^^

Main> Error: Undefined name hole0. 

(interactive):1:4--1:9
   |
 1 | :t hole0
   |    ^^^^^

Main> Error: Undefined name hole1. 

(interactive):1:4--1:9
   |
 1 | :t hole1
   |    ^^^^^

Main> Unknown name hole1
Main> Bye for now!