idris-0.9.12: Functional Programming Language with Dependent Types

Safe HaskellNone

Idris.Core.Typecheck

Documentation

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

isHole :: (t, Binder t1) -> BoolSource

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

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