idris

Safe HaskellNone

Idris.AbsSyntax

Contents

Synopsis

Documentation

forCodegen :: Codegen -> [(Codegen, a)] -> [a]Source

runIO :: IO a -> Idris aSource

A version of liftIO that puts errors into the exception type of the Idris monad

expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> [Name] -> PTerm -> PTermSource

expandParamsD :: Bool -> IState -> (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDeclSource

mapsnd :: (t -> t2) -> (t1, t) -> (t1, t2)Source

if it's just a type variable or concrete type, do it early (0)

if there's only type variables and injective constructors, do it next (1)

if there's a function type, next (2)

finally, everything else (3)

addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTermSource

aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTermSource

mkPApp :: FC -> Int -> PTerm -> [PArg] -> PTermSource

data EitherErr a b Source

Constructors

LeftErr a 
RightOK b 

Instances