idris-0.9.11.1: Functional Programming Language with Dependent Types

Safe HaskellNone

Idris.Core.Typecheck

Documentation

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

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

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

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

recheck :: 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