Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Generating a "Show" instance
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