Safe Haskell | None |
---|
- 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 a)] -> PTerm -> Idris ()
- 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 a => [TT a] -> [a] -> [Int] -> [a]
- getUniqueUsed :: Context -> Term -> [Name]
- getStaticNames :: IState -> Term -> [Name]
- getStatics :: [Name] -> Term -> [Bool]
- mkStatic :: [Name] -> PDecl -> PDecl
- mkStaticTy :: [Name] -> PTerm -> PTerm
Documentation
recheckC_borrowing :: Bool -> [Name] -> FC -> Env -> TT Name -> StateT IState (ErrorT Err IO) (Term, Type)Source
checkDef :: FC -> [(Name, (Int, Maybe Name, TT Name))] -> StateT IState (ErrorT Err IO) [(Name, (Int, Maybe Name, Term))]Source
checkAddDef :: Bool -> Bool -> FC -> [(Name, (Int, Maybe Name, TT Name))] -> StateT IState (ErrorT Err IO) [(Name, (Int, Maybe Name, Term))]Source
inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]Source
inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]Source
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.
paramNames :: Eq a => [TT a] -> [a] -> [Int] -> [a]Source
getUniqueUsed :: Context -> Term -> [Name]Source
getStaticNames :: IState -> Term -> [Name]Source
getStatics :: [Name] -> Term -> [Bool]Source
mkStaticTy :: [Name] -> PTerm -> PTermSource