SourceLoc.idr:12:19-25:
   |
12 | getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation
   |                   ~~~~~~~
This style of tactic proof is deprecated. See %runElab for the replacement.

SourceLoc.idr:21:19-23:
   |
21 | fromProofScript = proof sourceLocation
   |                   ~~~~~
This style of tactic proof is deprecated. See %runElab for the replacement.

SourceLoc.idr:41:20-26:
   |
41 |     Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t
   |                    ~~~~~~~
This style of tactic proof is deprecated. See %runElab for the replacement.

SourceLoc.idr:99:18-22:
   |
99 | SourceLoc.meta = proof
   |                  ~~~~~
This style of tactic proof is deprecated. See %runElab for the replacement.

Testing using definition
FileLoc "SourceLoc.idr" (17, 11) (17, 16)
Testing using inline tactics
FileLoc "SourceLoc.idr" (21, 19) (21, 38)
Testing using metavariable with later definition
FileLoc "SourceLoc.idr" (99, 18) (100, 16)
-----------------------
Success!
Error at FileLoc "SourceLoc.idr" (73, 23) (73, 25)
Success!
Success!