idris-0.12.3: test/ffi005/Postulate.idr
module Main %language TypeProviders bad : IO (Provider Type) bad = pure $ pure Void %provide postulate oops with bad main : IO () main = putStrLn "oops"
module Main %language TypeProviders bad : IO (Provider Type) bad = pure $ pure Void %provide postulate oops with bad main : IO () main = putStrLn "oops"