Documentation

data Command Source

data ElabState aux Source

type Elab' aux a = StateT (ElabState aux) TC aSource

type Elab a = Elab' () aSource

proof :: ElabState aux -> ProofStateSource

proofFail :: Elab' aux a -> Elab' aux aSource

saveState :: Elab' aux ()Source

loadState :: Elab' aux ()Source

errAt :: String -> Name -> Elab' aux a -> Elab' aux aSource

erun :: FC -> Elab' aux a -> Elab' aux aSource

runElab :: aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)Source

execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux)Source

initElaborator :: Name -> Context -> Type -> ProofStateSource

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

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

getAux :: Elab' aux auxSource

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

processTactic' :: (MonadTrans t, MonadState (ElabState aux) (t TC)) => Tactic -> t TC ()Source

get_context :: Elab' aux ContextSource

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

get_term :: Elab' aux TermSource

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

get_env :: Elab' aux EnvSource

get_holes :: Elab' aux [Name]Source

get_probs :: Elab' aux FailsSource

goal :: Elab' aux TypeSource

get_guess :: Elab' aux TypeSource

get_type :: Raw -> Elab' aux TypeSource

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

get_deferred :: Elab' aux [Name]Source

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

get_instances :: Elab' aux [Name]Source

unique_hole :: Name -> Elab' aux NameSource

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

uniqueNameCtxt :: Context -> Name -> [Name] -> Elab' aux NameSource

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

getLog :: Elab' aux StringSource

attack :: Elab' aux ()Source

claim :: Name -> 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

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 -> Raw -> Elab' aux ()Source

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

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

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

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

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

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

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

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

matchProblems :: Elab' aux ()Source

unifyProblems :: Elab' aux ()Source

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

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

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

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

proofstate :: Elab' aux ()Source

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

qed :: Elab' aux TermSource

undo :: Elab' aux ()Source

prepare_apply :: Raw -> [Bool] -> Elab' aux [Name]Source

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

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

apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [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 :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()Source

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

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

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

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

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

tryAll :: [(Elab' aux a, String)] -> Elab' aux aSource

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

qshow :: Fails -> StringSource

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

module Core.ProofState