TTImp.BindImplicits

Definitions

renameIBinds : List String -> List String -> RawImp -> State (List (String, String)) RawImp

Visibility: export

doBind : List (Name, Name) -> RawImp -> RawImp

Visibility: export

bindNames : Ref Ctxt Defs => Bool -> RawImp -> Core (List Name, RawImp)

Visibility: export

bindTypeNames : Ref Ctxt Defs => FC -> List (Maybe Name, RawImp) -> List Name -> RawImp -> Core RawImp

Visibility: export

bindTypeNamesUsed : Ref Ctxt Defs => FC -> List String -> List Name -> RawImp -> Core RawImp

Visibility: export

piBindNames : Ref Ctxt Defs => FC -> List Name -> RawImp -> Core RawImp

Visibility: export