TTImp.Elab.Utils

Definitions

findErased : Ref Ctxt Defs => ClosedTerm -> Core (List Nat, List Nat)

Visibility: export

updateErasable : Ref Ctxt Defs => Name -> Core ()

Visibility: export

wrapErrorC : List ElabOpt -> (Error -> Error) -> Core a -> Core a

Visibility: export

bindNotReq : FC -> Int -> Env Term vs -> SubVars pre vs -> List (PiInfo RawImp, Name) -> Term vs -> (List (PiInfo RawImp, Name), Term pre)

Visibility: export

bindReq : FC -> Env Term vs -> SubVars pre vs -> List (PiInfo RawImp, Name) -> Term pre -> Maybe (List (PiInfo RawImp, Name), (List Name, ClosedTerm))

Visibility: export

inlineSafe : CaseTree vars -> Core Bool

Visibility: export

canInlineDef : Ref Ctxt Defs => Name -> Core Bool

Visibility: export

canInlineCaseBlock : Ref Ctxt Defs => Name -> Core Bool

Visibility: export