idris-0.9.17: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Elab.Utils

Synopsis

Documentation

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.

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.

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

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

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

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

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