idris-1.3.4: Functional Programming Language with Dependent Types
LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellSafe-Inferred
LanguageHaskell2010

Idris.Core.Typecheck

Description

 

Documentation

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

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

isHole :: (a, b, Binder b) -> Bool Source #

errEnv :: [(a, b, Binder b)] -> [(a, b)] Source #

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

convType :: String -> Context -> Env -> Term -> StateT UCs TC () Source #

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

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

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

data UniqueUse Source #

Constructors

Never 
Once 
LendOnly 
Many 

Instances

Instances details
Eq UniqueUse Source # 
Instance details

Defined in Idris.Core.Typecheck

Methods

(==) :: UniqueUse -> UniqueUse -> Bool

(/=) :: UniqueUse -> UniqueUse -> Bool

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