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.print print-α begin      = "."
    Print.print print-α (step-α b) = "a" ++ print b

    Print.print print-β (step-β a) = "b" ++ print a