Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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