TTImp.Elab.Delayed

Definitions

delayOnFailure : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => FC -> RigCount -> Env Term vars -> Maybe (Glued vars) -> (Error -> Bool) -> DelayReason -> (Bool -> Core (Term vars, Glued vars)) -> Core (Term vars, Glued vars)

Visibility: export

delayElab : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => FC -> RigCount -> Env Term vars -> Maybe (Glued vars) -> DelayReason -> Core (Term vars, Glued vars) -> Core (Term vars, Glued vars)

Visibility: export

ambiguous : Error -> Bool

Visibility: export

recoverable : Ref Ctxt Defs => Error -> Core Bool

Visibility: export

retryDelayed : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => UnifyInfo -> List (DelayReason, (Int, (NameMap (), Core ClosedTerm))) -> Core ()

Visibility: export

runDelays : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref EST (EState vars) => (DelayReason -> Bool) -> Core a -> Core a

Visibility: export