TTImp.Utils

Definitions

genUniqueStr : List String -> String -> String

Visibility: export

findBindableNames : Bool -> List Name -> List String -> RawImp -> List (Name, Name)

Visibility: export

findUniqueBindableNames : Ref Ctxt Defs => FC -> Bool -> List Name -> List String -> RawImp -> Core (List (Name, Name))

Visibility: export

findAllNames : List Name -> RawImp -> List Name

Visibility: export

findIBindVars : RawImp -> List Name

Visibility: export

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

Visibility: export

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

Visibility: export

substNamesClause : List Name -> List (Name, RawImp) -> ImpClause -> ImpClause

Visibility: export

substLoc : FC -> RawImp -> RawImp

Visibility: export

substLocClause : FC -> ImpClause -> ImpClause

Visibility: export

uniqueBasicName : Defs -> List String -> String -> Core String

Visibility: export

uniqueHoleName : Ref Syn SyntaxInfo => Defs -> List String -> String -> Core String

Visibility: export

uniqueHoleNames : Ref Syn SyntaxInfo => Defs -> Nat -> String -> Core (List String)

Visibility: export

getArgName : Ref Ctxt Defs => Defs -> Name -> List Name -> List Name -> NF vars -> Core String

Visibility: export

getArgNames : Ref Ctxt Defs => Defs -> List Name -> List Name -> Env Term vars -> NF vars -> Core (List String)

Visibility: export

etaExpandImplicits : Ref Ctxt Defs => Ref UST UState => FC -> RawImp -> RawImp -> RawImp -> Core (RawImp, RawImp)

Visibility: export