Safe Haskell	None
Language	Haskell98

Idris.Elab.Utils

Synopsis

Documentation

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

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

iderr :: Name -> Err -> Err Source

checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))] -> Idris [(Name, (Int, Maybe Name, Type))] Source

checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))] -> Idris [(Name, (Int, Maybe Name, Type))] Source

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

Get the list of (index, name) of inaccessible arguments from an elaborated type

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

Get the list of (index, name) of inaccessible arguments from the type.

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

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

Check that the result of type checking matches what the programmer wrote (i.e. - if we inferred any arguments that the user provided, make sure they are the same!)

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

Return whether inferred term is different from given term (as above, but return a Bool)

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

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 Source

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

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

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

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

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

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

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

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

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

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

getStaticNames :: IState -> Term -> [Name] Source

getStatics :: [Name] -> Term -> [Bool] Source

mkStatic :: [Name] -> PDecl -> PDecl Source

mkStaticTy :: [Name] -> PTerm -> PTerm Source