:: Name	the name of what's to be elaborated
-> Context	the current global context
-> Ctxt TypeInfo	the value of the idris_datatypes field of IState
-> Int	the value of the idris_name field of IState
-> Type	the goal type
-> ProofState

elaborate :: Context -> Ctxt TypeInfo -> Int -> Name -> Type -> aux -> Elab' aux a -> TC (a, String) Source

updateAux :: (aux -> aux) -> Elab' aux () Source

Modify the auxiliary state

getAux :: Elab' aux aux Source

Get the auxiliary state

unifyLog :: Bool -> Elab' aux () Source

Set whether to show the unifier log

getUnifyLog :: Elab' aux Bool Source

processTactic' :: Tactic -> Elab' aux () Source

Process a tactic within the current elaborator state

updatePS :: (ProofState -> ProofState) -> Elab' aux () Source

now_elaborating :: FC -> Name -> Name -> Elab' aux () Source

done_elaborating_app :: Name -> Elab' aux () Source

done_elaborating_arg :: Name -> Name -> Elab' aux () Source

elaborating_app :: Elab' aux [(FC, Name, Name)] Source

get_context :: Elab' aux Context Source

Get the global context

set_context :: Context -> Elab' aux () Source

Update the context. (should only be used for adding temporary definitions or all sorts of stuff could go wrong)

get_datatypes :: Elab' aux (Ctxt TypeInfo) Source

set_datatypes :: Ctxt TypeInfo -> Elab' aux () Source

get_global_nextname :: Elab' aux Int Source

set_global_nextname :: Int -> Elab' aux () Source

get_term :: Elab' aux Term Source

get the proof term

update_term :: (Term -> Term) -> Elab' aux () Source

modify the proof term

get_env :: Elab' aux Env Source

get the local context at the currently in focus hole

get_inj :: Elab' aux [Name] Source

get_holes :: Elab' aux [Name] Source

get_usedns :: Elab' aux [Name] Source

get_probs :: Elab' aux Fails Source

get_recents :: Elab' aux [Name] Source

Return recently solved names (that is, the names solved since the last call to get_recents)

goal :: Elab' aux Type Source

get the current goal type

is_guess :: Elab' aux Bool Source

get_guess :: Elab' aux Term Source

Get the guess at the current hole, if there is one

get_type :: Raw -> Elab' aux Type Source

Typecheck locally

get_type_val :: Raw -> Elab' aux (Term, Type) Source

get_deferred :: Elab' aux [Name] Source

get holes we've deferred for later definition

checkInjective :: (Term, Term, Term) -> Elab' aux () Source

get_instances :: Elab' aux [Name] Source

get instance argument names

get_autos :: Elab' aux [(Name, ([FailContext], [Name]))] Source

get auto argument names

unique_hole :: Name -> Elab' aux Name Source

given a desired hole name, return a unique hole name

unique_hole' :: Bool -> Name -> Elab' aux Name Source

elog :: String -> Elab' aux () Source

getLog :: Elab' aux String Source

attack :: Elab' aux () Source

claim :: Name -> Raw -> Elab' aux () Source

claimFn :: Name -> Name -> Raw -> Elab' aux () Source

unifyGoal :: Raw -> Elab' aux () Source

unifyTerms :: Raw -> Raw -> Elab' aux () Source

exact :: Raw -> Elab' aux () Source

fill :: Raw -> Elab' aux () Source

match_fill :: Raw -> Elab' aux () Source

prep_fill :: Name -> [Name] -> Elab' aux () Source

complete_fill :: Elab' aux () Source

solve :: Elab' aux () Source

start_unify :: Name -> Elab' aux () Source

end_unify :: Elab' aux () Source

unify_all :: Elab' aux () Source

regret :: Elab' aux () Source

compute :: Elab' aux () Source

computeLet :: Name -> Elab' aux () Source

simplify :: Elab' aux () Source

hnf_compute :: Elab' aux () Source

eval_in :: Raw -> Elab' aux () Source

check_in :: Raw -> Elab' aux () Source

intro :: Maybe Name -> Elab' aux () Source

introTy :: Raw -> Maybe Name -> Elab' aux () Source

forall :: Name -> Maybe ImplicitInfo -> Raw -> Elab' aux () Source

letbind :: Name -> Raw -> Raw -> Elab' aux () Source

expandLet :: Name -> Term -> Elab' aux () Source

rewrite :: Raw -> Elab' aux () Source

induction :: Raw -> Elab' aux () Source

casetac :: Raw -> Elab' aux () Source

equiv :: Raw -> Elab' aux () Source

patvar :: Name -> Elab' aux () Source

Turn the current hole into a pattern variable with the provided name, made unique if MN

patvar' :: Name -> Elab' aux () Source

Turn the current hole into a pattern variable with the provided name, but don't make MNs unique.

patbind :: Name -> Elab' aux () Source

focus :: Name -> Elab' aux () Source

movelast :: Name -> Elab' aux () Source

dotterm :: Elab' aux () Source

get_dotterm :: Elab' aux [(Name, [Name])] Source

zipHere :: Elab' aux () Source

Set the zipper in the proof state to point at the current sub term (This currently happens automatically, so this will have no effect...)

matchProblems :: Bool -> Elab' aux () Source

unifyProblems :: Elab' aux () Source

defer :: [Name] -> Name -> Elab' aux Name Source

deferType :: Name -> Raw -> [Name] -> Elab' aux () Source

instanceArg :: Name -> Elab' aux () Source

autoArg :: Name -> Elab' aux () Source

setinj :: Name -> Elab' aux () Source

proofstate :: Elab' aux () Source

reorder_claims :: Name -> Elab' aux () Source

qed :: Elab' aux Term Source

undo :: Elab' aux () Source

prepare_apply Source

Arguments

:: Raw	The operation being applied
-> [Bool]	Whether arguments are implicit
-> Elab' aux [(Name, Name)]	The names of the arguments and their holes to be filled with elaborated argument values

Prepare to apply a function by creating holes to be filled by the arguments

apply Source

Arguments

:: Raw	The operator to apply
-> [(Bool, Int)]	For each argument, whether to attempt to solve it and the priority in which to do so
-> Elab' aux [(Name, Name)]

Apply an operator, solving some arguments by unification or matching.

match_apply Source

Arguments

:: Raw	The operator to apply
-> [(Bool, Int)]	For each argument, whether to attempt to solve it and the priority in which to do so
-> Elab' aux [(Name, Name)]

Apply an operator, solving some arguments by unification or matching.

apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)] Source

apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux () Source

apply_elab :: Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux () Source

checkPiGoal :: Name -> Elab' aux () Source

simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux () Source

infer_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux () Source

dep_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux () Source

arg :: Name -> Maybe ImplicitInfo -> Name -> Elab' aux () Source

no_errors :: Elab' aux () -> Maybe Err -> Elab' aux () Source

try :: Elab' aux a -> Elab' aux a -> Elab' aux a Source

handleError :: (Err -> Bool) -> Elab' aux a -> Elab' aux a -> Elab' aux a Source

try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a Source

tryCatch :: Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a Source

tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a Source

tryAll :: [(Elab' aux a, Name)] -> Elab' aux a Source

tryAll' :: Bool -> [(Elab' aux a, Name)] -> Elab' aux a Source

prunStateT :: Int -> Bool -> [a] -> Maybe [b] -> StateT (ElabState t) TC t1 -> ElabState t -> TC ((t1, Int, Fails), ElabState t) Source

debugElaborator :: [ErrorReportPart] -> Elab' aux a Source

qshow :: Fails -> String Source

dumpprobs :: Show a => [(t, t1, t2, a)] -> [Char] Source

module Idris.Core.ProofState