Skip to content

Instantly share code, notes, and snippets.

@derrickturk

derrickturk/typecase.idr

Created December 5, 2020 02:07
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 derrickturk/b4290d8c0a562aff11e87e9defee8f0f to your computer and use it in GitHub Desktop.
Save derrickturk/b4290d8c0a562aff11e87e9defee8f0f to your computer and use it in GitHub Desktop.
Download ZIP
Idris 2 - looks like typecase is back on the menu, boys!
Raw
typecase.idr
perverse : {a : Type} -> a -> a
perverse {a = Integer} x = x + 1
perverse {a = String} x = "hello " <+> x
perverse {a = _} x = x
main : IO ()
main = do
printLn $ perverse 5
printLn $ perverse "world"
printLn $ perverse True
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment