git.iko.soy/Idris-dev
on 5e2000e help sign in
Idris-dev/test/proof007/expected
10 lines 278 B history raw
1DefaultArgUnknownName.idr:9:8-23:
2 |
39 | test = funWithBadDefArg
4 | ~~~~~~~~~~~~~~~~
5When checking right hand side of test with expected type
6 ()
8When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:
9 No such variable sadgjhsag