src/Core/Term/Environment.idr


1
2
3
4
5
6
7
8
9
10
11
12
13

module Core.Term.Environment

import Core.Context
import Core.Term

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

public export
data Env : Context -> Type where
  Lin : Env [<]
  (:<) : Env sx -> Term sx -> Env (sx :< n)

%name Env env