proof010.idr

data MyShow : Type -> Type where
     ShowImplementation : (show : a -> String) -> MyShow a

myshow : {auto inst : MyShow a} -> a -> String
myshow {inst = ShowImplementation show} x1 = show x1

%hint
showNat : MyShow Nat
showNat = ShowImplementation show

%hint
showFn : MyShow (a -> b)
showFn = ShowImplementation (\x => "<< function >>")

%hint
showBools : MyShow (Bool, Bool)
showBools = ShowImplementation (\x => "some bools")

%hint
showStuff : MyShow a -> MyShow b -> MyShow (a, b)
showStuff sa sb = ShowImplementation showPair
  where
    showPair : (a, b) -> String
    showPair (x, y) = myshow x ++ ", " ++ myshow y

testShow : List (Bool, Bool) -> String
testShow [] = "" 
testShow (x :: xs) = myshow x ++ "\n" ++ testShow xs

testShow2 : List (Nat, Int -> Int) -> String
testShow2 [] = "" 
testShow2 (x :: xs) = myshow x ++ "\n" ++ testShow2 xs

main : IO ()
main = do putStrLn $ testShow2 [(2, (+1)), (3, abs)]
          putStrLn $ testShow [(True, False), (False, True)]