Skip to content

Instantly share code, notes, and snippets.

@david-christiansen

david-christiansen/ClassNonsense.idr

Created June 17, 2015 17:29
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save david-christiansen/e33084ca9d2fadcdefbe to your computer and use it in GitHub Desktop.
Save david-christiansen/e33084ca9d2fadcdefbe to your computer and use it in GitHub Desktop.
Download ZIP
Raw
ClassNonsense.idr
module ClassNonsense
import Language.Reflection.Elab
class Foo t where
constructor MkFoo
foo : t
myFoo : Foo Nat
myFoo = MkFoo 1
forEffect : ()
forEffect =
%runElab (do
addInstance `{Foo} `{myFoo}
search)
bar : Nat
bar = foo
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment