» idris FileDSL.idr -o file
Resimp.idr:125:32:The use of [static] is deprecated, use %static instead.
Resimp.idr:123:9:Use of deprecated name Prelude.Monad.return
Please use `pure`, which is equivalent.
Resimp.idr:132:10:Use of deprecated name Prelude.Monad.return
Please use `pure`, which is equivalent.
Resimp.idr:135:10:Use of deprecated name Prelude.Monad.return
Please use `pure`, which is equivalent.
Resimp.idr:144:10:Use of deprecated name Prelude.Monad.return
Please use `pure`, which is equivalent.
Resimp.idr:154:10:Use of deprecated name Prelude.Monad.return
Please use `pure`, which is equivalent.
You must turn on the DSLNotation extension to use a dsl block
