Instance.agda

open import Data.String


record Print (A : Set) : Set where
  field
    print : A → String
open Print {{…}} public

mutual
  data α : Set where
    begin : α
    step-α : β → α

  data β : Set where
    step-β : α → β

example : α
example = step-α (step-β begin)

mutual
  instance
    print-α : Print α
    print-β : Print β

    print-α = record { print = λ {begin → "."
                               ; (step-α b) → "a" ++ (print b)} }
    print-β = record { print = λ {(step-β a) → "b" ++ (print a)} }