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