module Core.Term.Thinned

import Core.Term
import Core.Thinning

%prefix_record_projections off

infix 4 =~=

-- Definition ------------------------------------------------------------------

public export
record Thinned (n : Nat) where
  constructor Over
  {0 m : Nat}
  term : Term m
  thin : m `Thins` n

%name Thinned t, u, v

%inline
public export
expand : Thinned n -> Term n
expand (term `Over` thin) = wkn term thin

public export
(=~=) : Thinned n -> Thinned n -> Type
t =~= u = expand t = expand u

-- Weakening -------------------------------------------------------------------

public export
wkn : Thinned m -> m `Thins` n -> Thinned n
wkn t thin = { thin $= (thin .) } t