module abridgement where

open import Data.Nat

record env : Set where
  field
    a : !$\mathbb{N}$!
    b : !$\mathbb{N}$!
    c : !$\mathbb{N}$!
open env

patternmatch-default : env !$\rightarrow$! !$\mathbb{N}$!
patternmatch-default record { a = a ; b = b ; c = c } = c

patternmatch-extraction : env !$\rightarrow$! !$\mathbb{N}$!
patternmatch-extraction env with c env
patternmatch-extraction env | c = c

patternmatch-extraction!$\prime$! : env !$\rightarrow$! !$\mathbb{N}$!
patternmatch-extraction!$\prime$! env with c env
... | c = c