idris-0.12.2: Functional Programming Language with Dependent Types

CopyrightLicense : BSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell98

Idris.Core.Typecheck

Description

 

Documentation

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 #

data UniqueUse Source #

Constructors

Never 
Once 
LendOnly 
Many 

Instances

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