Core.Env

Definitions

data Env : Scoped -> Scope -> Type

Totality: total
Visibility: public export
Constructors:

Nil : Env tm empty

(::) : Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)

Hints:

HasNames (Env Term vars)

TTC (Env Term vars)

empty : Env tm empty

Totality: total
Visibility: public export

extend : (x : Name) -> Binder (tm vars) -> Env tm vars -> Env tm (x :: vars)

Totality: total
Visibility: export

(++) : Env Term ns -> Env Term vars -> Env Term (ns ++ vars)

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

length : Env tm xs -> Nat

Totality: total
Visibility: export

lengthNoLet : Env tm xs -> Nat

Totality: total
Visibility: export

lengthExplicitPi : Env tm xs -> Nat

Totality: total
Visibility: export

namesNoLet : Env tm xs -> List Name

Totality: total
Visibility: export

eraseLinear : Env tm vs -> Env tm vs

Totality: total
Visibility: export

getErased : Env tm vs -> List (Var vs)

Totality: total
Visibility: export

data IsDefined : Name -> Scope -> Type

Totality: total
Visibility: public export
Constructor: 

MkIsDefined : RigCount -> (0 _ : IsVar n idx vars) -> IsDefined n vars

defined : (n : Name) -> Env Term vars -> Maybe (IsDefined n vars)

Totality: total
Visibility: export

bindEnv : FC -> Env Term vars -> Term vars -> ClosedTerm

Totality: total
Visibility: export

getBinder : Weaken tm => (0 _ : IsVar x idx vars) -> Env tm vars -> Binder (tm vars)

Totality: total
Visibility: export

getBinderLoc : (0 _ : IsVar x idx vars) -> Env tm vars -> FC

Totality: total
Visibility: export

abstractEnvType : FC -> Env Term vars -> Term vars -> ClosedTerm

Totality: total
Visibility: export

abstractEnv : FC -> Env Term vars -> Term vars -> ClosedTerm

Totality: total
Visibility: export

abstractFullEnvType : FC -> Env Term vars -> Term vars -> ClosedTerm

Totality: total
Visibility: export

mkExplicit : Env Term vs -> Env Term vs

Totality: total
Visibility: export

letToLam : Env Term vars -> Env Term vars

Totality: total
Visibility: export

findUsedLocs : Env Term vars -> Term vars -> VarSet vars

Totality: total
Visibility: export

findSubEnv : Env Term vars -> Term vars -> (vars' : Scope ** Thin vars' vars)

Totality: total
Visibility: export

shrinkEnv : Env Term vars -> Thin newvars vars -> Maybe (Env Term newvars)

Totality: total
Visibility: export

mkEnvOnto : FC -> (xs : List Name) -> Env Term ys -> Env Term (xs ++ ys)

Totality: total
Visibility: export

mkEnv : FC -> (vs : Scope) -> Env Term vs

Totality: total
Visibility: export

uniqifyEnv : Env Term vars -> (vars' : List Name ** (Env Term vars', CompatibleVars vars vars'))

Totality: total
Visibility: export

allVars : Env Term vars -> List (Var vars)

Totality: total
Visibility: export

allVarsNoLet : Env Term vars -> List (Var vars)

Totality: total
Visibility: export

close : FC -> String -> Env Term vars -> Term vars -> ClosedTerm

Totality: total
Visibility: export