Idris2/tests/node/idiom001/Main.idr

mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-16 07:34:45 +03:00
main : IO ()
main = do
  [| (const $ pure MkUnit) (pure ()) |]
  pure ()
Make `NmLet` names unique in `Compiler.ES.Imperative` Since the imperative form has no nesting of scopes. Fixes #643 2020-09-19 22:09:36 +03:00			`main : IO ()`
			`main = do`
			`[\| (const $ pure MkUnit) (pure ()) \|]`
Remove trailing whitespaces and add trailing newlines 2021-01-16 10:03:45 +03:00			`pure ()`