Creating a simple function in Idris for you to play with

Foo.idr

module Foo

public export
data Foo = Try Int | Again Int

implementation Show Foo where
  show (Try n) = "(Try " ++ (show n) ++ ")"
  show (Again n) = "(Again " ++ (show n) ++ ")"

export
bar : Foo -> String
bar = show

-- but suppose we have a double in the mix
-- Now, this is isomorphic to Either Int Double

public export
data NewFoo = NTry Int | NAgain Double

export
qux : NewFoo -> Either Int Double
qux (NTry n) = Left n
qux (NAgain d) = Right d