idris-1.3.1: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.Core.Typecheck

Description

 

Documentation

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

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

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

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

data UniqueUse Source #

Constructors

Never 
Once 
LendOnly 
Many 
Instances
Eq UniqueUse Source # 
Instance details

Defined in Idris.Core.Typecheck

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