git.iko.soy/Idris-dev
on fdfd99e help sign in
Idris-dev/test/proof007/DefaultArgUnknownName.idr
10 lines 235 B history raw
1module DefaultArgUnknownName
3-- FIXME: What is the expected behaviour here? Should the type declaration
4-- not compile?
5funWithBadDefArg : { default sadgjhsag arg : () } -> ()
6funWithBadDefArg = ()
8test : ()
9test = funWithBadDefArg