packages feed

idris-0.9.17.1: test/proof007/DefaultArgUnknownName.idr

module DefaultArgUnknownName

-- FIXME: What is the expected behaviour here? Should the type declaration
-- not compile?
funWithBadDefArg : { default sadgjhsag arg : () } -> ()
funWithBadDefArg = ()

test : ()
test = funWithBadDefArg