:: NameType
-> [(Name, (Int, Maybe Name, Type, Bool))]	The Name is the name being made into a metavar, the Int is the number of vars that are part of a putative proof context, the Maybe Name is the top-level function containing the new metavariable, the Type is its type, and the Bool is whether :p is allowed
-> Idris ()

Save information about a name that is not yet defined

solveDeferred :: Name -> Idris () Source

getUndefined :: Idris [Name] Source

isMetavarName :: Name -> IState -> Bool Source

getWidth :: Idris ConsoleWidth Source

setWidth :: ConsoleWidth -> Idris () Source

type1Doc :: Doc OutputAnnotation Source

isetPrompt :: String -> Idris () Source

isetLoadedRegion :: Idris () Source

Tell clients how much was parsed and loaded

setLogLevel :: Int -> Idris () Source

setCmdLine :: [Opt] -> Idris () Source

getCmdLine :: Idris [Opt] Source

getDumpDefun :: Idris (Maybe FilePath) Source

getDumpCases :: Idris (Maybe FilePath) Source

logLevel :: Idris Int Source

setErrContext :: Bool -> Idris () Source

errContext :: Idris Bool Source

getOptimise :: Idris [Optimisation] Source

setOptimise :: [Optimisation] -> Idris () Source

addOptimise :: Optimisation -> Idris () Source

removeOptimise :: Optimisation -> Idris () Source

setOptLevel :: Int -> Idris () Source

useREPL :: Idris Bool Source

setREPL :: Bool -> Idris () Source

showOrigErr :: Idris Bool Source

setShowOrigErr :: Bool -> Idris () Source

setAutoSolve :: Bool -> Idris () Source

setNoBanner :: Bool -> Idris () Source

getNoBanner :: Idris Bool Source

setQuiet :: Bool -> Idris () Source

getQuiet :: Idris Bool Source

setCodegen :: Codegen -> Idris () Source

codegen :: Idris Codegen Source

setOutputTy :: OutputType -> Idris () Source

outputTy :: Idris OutputType Source

setIdeMode :: Bool -> Handle -> Idris () Source

setTargetTriple :: String -> Idris () Source

targetTriple :: Idris String Source

setTargetCPU :: String -> Idris () Source

targetCPU :: Idris String Source

verbose :: Idris Bool Source

setVerbose :: Bool -> Idris () Source

typeInType :: Idris Bool Source

setTypeInType :: Bool -> Idris () Source

coverage :: Idris Bool Source

setCoverage :: Bool -> Idris () Source

setIBCSubDir :: FilePath -> Idris () Source

valIBCSubDir :: IState -> Idris FilePath Source

addImportDir :: FilePath -> Idris () Source

setImportDirs :: [FilePath] -> Idris () Source

allImportDirs :: Idris [FilePath] Source

colourise :: Idris Bool Source

setColourise :: Bool -> Idris () Source

impShow :: Idris Bool Source

setImpShow :: Bool -> Idris () Source

setColour :: ColourType -> IdrisColour -> Idris () Source

logLvl :: Int -> String -> Idris () Source

cmdOptType :: Opt -> Idris Bool Source

iLOG :: String -> Idris () Source

noErrors :: Idris Bool Source

setTypeCase :: Bool -> Idris () Source

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

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

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)

getPriority :: IState -> PTerm -> Int Source

addStatics :: Name -> Term -> PTerm -> Idris () Source

addToUsing :: [Using] -> [(Name, PTerm)] -> [Using] Source

addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm Source

addUsingImpls :: SyntaxInfo -> Name -> FC -> PTerm -> Idris PTerm Source

getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)] Source

implicit :: ElabInfo -> SyntaxInfo -> Name -> PTerm -> Idris PTerm Source

implicit' :: ElabInfo -> SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm Source

implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg]) Source

addImplPat :: IState -> PTerm -> PTerm Source

addImplBound :: IState -> [Name] -> PTerm -> PTerm Source

addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm Source

addImpl :: [Name] -> IState -> PTerm -> PTerm Source

Add the implicit arguments to applications in the term [Name] gives the names to always expend, even when under a binder of that name (this is to expand methods with implicit arguments in dependent type classes).

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

aiFn :: Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> [[Text]] -> [PArg] -> Either Err PTerm Source

stripLinear :: IState -> PTerm -> PTerm Source

stripUnmatchable :: IState -> PTerm -> PTerm Source

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

findStatics :: IState -> PTerm -> (PTerm, [Bool]) Source

data EitherErr a b Source

Constructors

LeftErr a
RightOK b

Instances

Monad (EitherErr a)
Functor (EitherErr a)
Applicative (EitherErr a)

toEither :: EitherErr a b -> Either a b Source

matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)] Source

matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)] Source

substMatches :: [(Name, PTerm)] -> PTerm -> PTerm Source

substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm Source

substMatch :: Name -> PTerm -> PTerm -> PTerm Source

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

shadow :: Name -> Name -> PTerm -> PTerm Source

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

module Idris.AbsSyntaxTree