Skip to content

Instantly share code, notes, and snippets.

@deque-blog

deque-blog/double_it_evaluation.idr

Last active June 13, 2017 12:41
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save deque-blog/1ecf10d3999c327230a434dd12f82cdf to your computer and use it in GitHub Desktop.
Save deque-blog/1ecf10d3999c327230a434dd12f82cdf to your computer and use it in GitHub Desktop.
Download ZIP
Raw
double_it_evaluation.idr
[*src/InOut> double_it
io_bind (io_bind prim_read
(\x =>
io_pure (prim__strRev (with block in Prelude.Interactive.getLine', trimNL (MkFFI C_Types String String)
(prim__strRev x)
(with block in Prelude.Strings.strM (prim__strRev x)
(Decidable.Equality.Bool implementation of Decidable.Equality.DecEq, method decEq (not (intToBool (prim__eqString (prim__strRev x)
"")))
True))))))
(\input =>
io_bind (prim_write (prim__concat (prim__toStrInt (prim__mulInt (prim__fromStrInt input) 2)) "\n"))
(\__bindx => io_pure ())) : IO ()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment