idris-0.9.17.1: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Core.Typecheck

Documentation

convertsC :: Context -> Env -> Term -> Term -> StateT UCs TC () Source

converts :: Context -> Env -> Term -> Term -> TC () Source

isHole :: (t, Binder t1) -> Bool Source

errEnv :: [(t, Binder t1)] -> [(t, t1)] Source

isType :: Context -> Env -> Term -> TC () Source

recheck :: Context -> Env -> Raw -> Term -> TC (Term, Type, UCs) Source

recheck_borrowing :: Bool -> [Name] -> Context -> Env -> Raw -> Term -> TC (Term, Type, UCs) Source

check :: Context -> Env -> Raw -> TC (Term, Type) Source

check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type) Source

data UniqueUse Source

Constructors

Never 
Once 
LendOnly 
Many 

Instances

checkUnique :: [Name] -> Context -> Env -> Term -> TC () Source