idris-0.9.15.1: Functional Programming Language with Dependent Types

Safe HaskellNone

Idris.Elab.Utils

Synopsis

Documentation

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.

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

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

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

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

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