Core.AutoSearch

Definitions

record ArgInfo : Scope -> Type

Totality: total
Visibility: public export
Constructor: 

MkArgInfo : Int -> RigCount -> PiInfo (Closure vars) -> Term vars -> Term vars -> ArgInfo vars

Projections:

.argRig : ArgInfo vars -> RigCount

.argType : ArgInfo vars -> Term vars

.holeID : ArgInfo vars -> Int

.metaApp : ArgInfo vars -> Term vars

.plicit : ArgInfo vars -> PiInfo (Closure vars)

.holeID : ArgInfo vars -> Int

Visibility: public export

holeID : ArgInfo vars -> Int

Visibility: public export

.argRig : ArgInfo vars -> RigCount

Visibility: public export

argRig : ArgInfo vars -> RigCount

Visibility: public export

.plicit : ArgInfo vars -> PiInfo (Closure vars)

Visibility: public export

plicit : ArgInfo vars -> PiInfo (Closure vars)

Visibility: public export

.metaApp : ArgInfo vars -> Term vars

Visibility: public export

metaApp : ArgInfo vars -> Term vars

Visibility: public export

.argType : ArgInfo vars -> Term vars

Visibility: public export

argType : ArgInfo vars -> Term vars

Visibility: public export

mkArgs : Ref Ctxt Defs => Ref UST UState => FC -> RigCount -> Env Term vars -> NF vars -> Core (List (ArgInfo vars), NF vars)

Visibility: export

impLast : List (ArgInfo vars) -> List (ArgInfo vars)

Visibility: export