idris

Safe HaskellNone

Core.Elaborate

Documentation

data Command Source

Constructors

Theorem Name Raw 
Eval Raw 
Quit 
Print Name 
Tac (Elab ()) 

data ElabState aux Source

Constructors

ES (ProofState, aux) String (Maybe (ElabState aux)) 

Instances

Show aux => Show (ElabState aux) 

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

type Elab a = Elab' () aSource

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

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

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

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

getAux :: Elab' aux auxSource

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

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

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

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

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

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

solve :: Elab' aux ()Source

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

check_in :: Raw -> 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

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

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

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

undo :: Elab' aux ()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

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

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