Copattern matching

copattern.agda

{-# OPTIONS --copatterns #-}
module copattern where

record Bar : Set where
    field 
        x : List Unit
        y : Unit
        z : ℕ
open Bar

-- define a record the usual way
_ : Bar
_ = record { x = cons unit nil ; y = unit ; z = 2 }       

-- define a record using copatterns
b : Bar
x b = cons unit nil
y b = unit
z b = 2