Safe Haskell | None |
---|
- data Command
- data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
- type Elab' aux a = StateT (ElabState aux) TC a
- type Elab a = Elab' () a
- proof :: ElabState aux -> ProofState
- proofFail :: Elab' aux a -> Elab' aux a
- explicit :: Name -> Elab' aux ()
- saveState :: Elab' aux ()
- loadState :: Elab' aux ()
- getNameFrom :: Name -> Elab' aux Name
- setNextName :: Elab' aux ()
- initNextNameFrom :: [Name] -> Elab' aux ()
- errAt :: String -> Name -> Elab' aux a -> Elab' aux a
- erun :: FC -> Elab' aux a -> Elab' aux a
- runElab :: aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
- execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux)
- initElaborator :: Name -> Context -> Type -> ProofState
- elaborate :: Context -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)
- force_term :: Elab' aux ()
- updateAux :: (aux -> aux) -> Elab' aux ()
- getAux :: Elab' aux aux
- unifyLog :: Bool -> Elab' aux ()
- getUnifyLog :: Elab' aux Bool
- processTactic' :: (MonadTrans t, MonadState (ElabState aux) (t (TC' Err))) => Tactic -> t (TC' Err) ()
- get_context :: Elab' aux Context
- set_context :: Context -> Elab' aux ()
- get_term :: Elab' aux Term
- update_term :: (Term -> Term) -> Elab' aux ()
- get_env :: Elab' aux Env
- get_holes :: Elab' aux [Name]
- get_probs :: Elab' aux Fails
- goal :: Elab' aux Type
- get_guess :: Elab' aux Type
- get_type :: Raw -> Elab' aux Type
- get_type_val :: Raw -> Elab' aux (Term, Type)
- get_deferred :: Elab' aux [Name]
- checkInjective :: (Term, Term, Term) -> Elab' aux ()
- get_instances :: Elab' aux [Name]
- unique_hole :: Name -> Elab' aux Name
- unique_hole' :: Bool -> Name -> Elab' aux Name
- elog :: String -> Elab' aux ()
- getLog :: Elab' aux String
- attack :: Elab' aux ()
- claim :: Name -> Raw -> Elab' aux ()
- exact :: Raw -> Elab' aux ()
- fill :: Raw -> Elab' aux ()
- match_fill :: Raw -> Elab' aux ()
- prep_fill :: Name -> [Name] -> Elab' aux ()
- complete_fill :: Elab' aux ()
- solve :: Elab' aux ()
- start_unify :: Name -> Elab' aux ()
- end_unify :: Elab' aux ()
- regret :: Elab' aux ()
- compute :: Elab' aux ()
- computeLet :: Name -> Elab' aux ()
- simplify :: Elab' aux ()
- hnf_compute :: Elab' aux ()
- eval_in :: Raw -> Elab' aux ()
- check_in :: Raw -> Elab' aux ()
- intro :: Maybe Name -> Elab' aux ()
- introTy :: Raw -> Maybe Name -> Elab' aux ()
- forall :: Name -> Raw -> Elab' aux ()
- letbind :: Name -> Raw -> Raw -> Elab' aux ()
- expandLet :: Name -> Term -> Elab' aux ()
- rewrite :: Raw -> Elab' aux ()
- induction :: Name -> Elab' aux ()
- equiv :: Raw -> Elab' aux ()
- patvar :: Name -> Elab' aux ()
- patbind :: Name -> Elab' aux ()
- focus :: Name -> Elab' aux ()
- movelast :: Name -> Elab' aux ()
- matchProblems :: Elab' aux ()
- unifyProblems :: Elab' aux ()
- defer :: Name -> Elab' aux ()
- deferType :: Name -> Raw -> [Name] -> Elab' aux ()
- instanceArg :: Name -> Elab' aux ()
- setinj :: Name -> Elab' aux ()
- proofstate :: Elab' aux ()
- reorder_claims :: Name -> Elab' aux ()
- qed :: Elab' aux Term
- undo :: Elab' aux ()
- prepare_apply :: Raw -> [Bool] -> Elab' aux [(Name, Name)]
- apply :: Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
- match_apply :: Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
- apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
- apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()
- apply_elab :: Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux ()
- checkPiGoal :: Name -> Elab' aux ()
- simple_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
- arg :: Name -> Name -> Elab' aux ()
- no_errors :: Elab' aux () -> Maybe Err -> Elab' aux ()
- try :: Elab' aux a -> Elab' aux a -> Elab' aux a
- try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
- tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a
- tryAll :: [(Elab' aux a, String)] -> Elab' aux a
- prunStateT :: Int -> Bool -> [a] -> StateT (ElabState t) (TC' Err) t1 -> ElabState t -> TC' Err ((t1, Int), ElabState t)
- qshow :: Fails -> String
- dumpprobs :: Show a => [(t, t1, t2, a)] -> [Char]
- module Idris.Core.ProofState
Documentation
ES (ProofState, aux) String (Maybe (ElabState aux)) |
proof :: ElabState aux -> ProofStateSource
getNameFrom :: Name -> Elab' aux NameSource
setNextName :: Elab' aux ()Source
initNextNameFrom :: [Name] -> Elab' aux ()Source
initElaborator :: Name -> Context -> Type -> ProofStateSource
force_term :: Elab' aux ()Source
getUnifyLog :: Elab' aux BoolSource
processTactic' :: (MonadTrans t, MonadState (ElabState aux) (t (TC' Err))) => Tactic -> t (TC' Err) ()Source
get_context :: Elab' aux ContextSource
set_context :: Context -> Elab' aux ()Source
update_term :: (Term -> Term) -> Elab' aux ()Source
get_deferred :: Elab' aux [Name]Source
get_instances :: Elab' aux [Name]Source
unique_hole :: Name -> Elab' aux NameSource
match_fill :: Raw -> Elab' aux ()Source
complete_fill :: Elab' aux ()Source
start_unify :: Name -> Elab' aux ()Source
computeLet :: Name -> Elab' aux ()Source
hnf_compute :: Elab' aux ()Source
matchProblems :: Elab' aux ()Source
unifyProblems :: Elab' aux ()Source
instanceArg :: Name -> Elab' aux ()Source
proofstate :: Elab' aux ()Source
reorder_claims :: Name -> Elab' aux ()Source
:: 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
checkPiGoal :: Name -> Elab' aux ()Source
prunStateT :: Int -> Bool -> [a] -> StateT (ElabState t) (TC' Err) t1 -> ElabState t -> TC' Err ((t1, Int), ElabState t)Source
module Idris.Core.ProofState