module OpClassesRepro

record SemigroupRec (t : Type) (op : t -> t -> t) where
    constructor SemigroupInfo
    associative : (a : t) -> (b : t) -> (c : t) -> (op (op a b) c = op a (op b c))

resolveSemigroup
  :  {auto associative : (a : t) -> (b : t) -> (c : t) -> (op (op a b) c = op a (op b c))}
  -> SemigroupRec t op
resolveSemigroup {associative} = SemigroupInfo associative

%hint
addAssoc
  : (a : Nat) -> (b : Nat) -> (c : Nat) -> plus (plus a b) c = plus a (plus b c)
addAssoc a b c = sym (plusAssociative a b c)

%hint
create : SemigroupRec Nat Prelude.Nat.plus
create = resolveSemigroup