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
 1 | import Data.Vect
 2 | import Data.Fin
 3 | 
 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
 3 | 
 4 | Vect_ext : (v : Vect n a) -> (w : Vect n a) -> ((i : Fin n) -> index i v = index i w)
 5 |   -> v = w
 6 | 
 7 | Weird : (v: Vect n a) -> v = v
                              ^^^^^

Error: No type declaration for Main.Weird.

Holes.idr:8:1--8:41
 4 | Vect_ext : (v : Vect n a) -> (w : Vect n a) -> ((i : Fin n) -> index i v = index i w)
 5 |   -> v = w
 6 | 
 7 | Weird : (v: Vect n a) -> v = v
 8 | Weird v =  Vect_ext ?hole0 ?hole1 ?hole2
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

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

Holes.idr:10:5--10:9
 06 | 
 07 | Weird : (v: Vect n a) -> v = v
 08 | Weird v =  Vect_ext ?hole0 ?hole1 ?hole2
 09 | 
 10 | f : Bool -> Nat
          ^^^^

Error: No type declaration for Main.f.

Holes.idr:11:1--11:11
 07 | Weird : (v: Vect n a) -> v = v
 08 | Weird v =  Vect_ext ?hole0 ?hole1 ?hole2
 09 | 
 10 | f : Bool -> Nat
 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!