Skip to content

Instantly share code, notes, and snippets.

@david-christiansen

david-christiansen/MkMonoid.idr

Created April 24, 2015 10:51
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 1 You must be signed in to fork a gist
  • Save david-christiansen/ccf9fccb9c1e021fd8b5 to your computer and use it in GitHub Desktop.
Save david-christiansen/ccf9fccb9c1e021fd8b5 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
MkMonoid.idr
module MkMonoid
import Language.Reflection.Elab
||| Generate a Monoid dictionary
total
mkMonoid : Semigroup a => (neutral : a) -> Monoid a
mkMonoid @{semigroup} neutral = mkMonoid' _ semigroup neutral
where
mkMonoid' : (a : Type) -> (constr : Semigroup a) -> a -> Monoid a
mkMonoid' = %runElab (fill (Var (SN (InstanceCtorN `{Monoid}))) *> solve)
instance Semigroup () where
(<+>) () () = ()
foo : Monoid ()
foo = mkMonoid ()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment