expected

DataDef.idr:74:1-8:
   |
74 | %runElab nope
   | ~~~~~~~~
While running an elaboration script, the following error occurred:
Prelude.Either.Either is already defined as a datatype.

Tacs.idr:299:17-300:78:
    |
299 |     testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))
    |                 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
When checking right hand side of testElab3 with expected type
        DPair Ty (Tm [])

Unifying ty and ARR ty t would lead to infinite value

AgdaStyleReflection.idr:315:7-20:
    |
315 | baz = tactic trivial
    |       ~~~~~~~~~~~~~~
When checking right hand side of baz with expected type
        (Nat, Void)

PROOF SEARCH FAILURE is not defined.