Idris.Elab.Utils

Documentation

recheckC :: FC -> Env -> TT Name -> StateT IState (ErrorT Err IO) (Term, Type)

recheckC_borrowing :: Bool -> [Name] -> FC -> Env -> TT Name -> StateT IState (ErrorT Err IO) (Term, Type)

checkDef :: FC -> [(Name, (Int, Maybe Name, TT Name))] -> StateT IState (ErrorT Err IO) [(Name, (Int, Maybe Name, Term))]

checkAddDef :: Bool -> Bool -> FC -> [(Name, (Int, Maybe Name, TT Name))] -> StateT IState (ErrorT Err IO) [(Name, (Int, Maybe Name, Term))]

inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]

inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()

checkInferred :: FC -> PTerm -> PTerm -> Idris ()

inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

checkDocs :: FC -> [(Name, Docstring)] -> PTerm -> Idris ()

Check a PTerm against documentation and ensure that every documented argument actually exists. This must be run _after_ implicits have been found, or it will give spurious errors.

decorateid :: (Name -> Name) -> PDecl' PTerm -> PDecl' PTerm

pbinds :: IState -> Term -> ElabD ()

pbty :: TT n -> TT n -> TT n

getPBtys :: TT t -> [(t, TT t)]

psolve :: TT t -> StateT (ElabState aux) TC ()

pvars :: IState -> TT Name -> [(Name, PTerm)]

getFixedInType :: IState -> [Name] -> [PArg' t] -> TT Name -> [Name]

getFlexInType :: IState -> [Name] -> [Name] -> TT Name -> [Name]

getParamsInType :: IState -> [Name] -> [PArg' t] -> TT Name -> [Name]

paramNames :: Eq t => [TT t] -> [t] -> [Int] -> [t]

getUniqueUsed :: Context -> Term -> [Name]