git.iko.soy/Idris-dev
on 5e2000e help sign in
Idris-dev/test/sourceLocation001/expected
35 lines 1.1 kB history raw
1SourceLoc.idr:12:19-25:
2 |
312 | getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation
4 | ~~~~~~~
5This style of tactic proof is deprecated. See %runElab for the replacement.
7SourceLoc.idr:21:19-23:
8 |
921 | fromProofScript = proof sourceLocation
10 | ~~~~~
11This style of tactic proof is deprecated. See %runElab for the replacement.
13SourceLoc.idr:41:20-26:
14 |
1541 | Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t
16 | ~~~~~~~
17This style of tactic proof is deprecated. See %runElab for the replacement.
19SourceLoc.idr:99:18-22:
20 |
2199 | SourceLoc.meta = proof
22 | ~~~~~
23This style of tactic proof is deprecated. See %runElab for the replacement.
25Testing using definition
26FileLoc "SourceLoc.idr" (17, 11) (17, 16)
27Testing using inline tactics
28FileLoc "SourceLoc.idr" (21, 19) (21, 38)
29Testing using metavariable with later definition
30FileLoc "SourceLoc.idr" (99, 18) (100, 16)
31-----------------------
32Success!
33Error at FileLoc "SourceLoc.idr" (73, 23) (73, 25)
34Success!
35Success!