Skip to content

Instantly share code, notes, and snippets.

@david-christiansen

david-christiansen/MkShow.idr

Last active October 26, 2017 21:35
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 1 You must be signed in to fork a gist
  • Save david-christiansen/1e6e17ec7637cde6d074 to your computer and use it in GitHub Desktop.
Save david-christiansen/1e6e17ec7637cde6d074 to your computer and use it in GitHub Desktop.
Download ZIP
Generating a "Show" instance
Raw
MkShow.idr
module MkShow
import Language.Reflection.Elab
mkShow : (a : Type) -> (a -> String) -> Show a
mkShow = %runElab (fill (Var (SN (InstanceCtorN `{Show}))) *> solve)
shower : Show Float
shower = mkShow _ (const "oops")
normalShow : show 3.2 = "3.2"
normalShow = Refl
myShow : show @{shower} 3.2 = "oops"
myShow = Refl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment