TTImp.Interactive.ExprSearch

Definitions

one : a -> Core (Search a)

Visibility: export

noResult : Core (Search a)

Visibility: export

searchN : Ref Ctxt Defs => Ref UST UState => Nat -> Core (Search a) -> Core (List a, Core (Search a))

Visibility: export

searchSort : Ref Ctxt Defs => Ref UST UState => Nat -> Core (Search a) -> (a -> a -> Ordering) -> Core (Search a)

Visibility: export

nextResult : Ref Ctxt Defs => Ref UST UState => Core (Search a) -> Core (Maybe (a, Core (Search a)))

Visibility: export

record SearchOpts : Type

Totality: not strictly positive
Visibility: public export
Constructor: 

MkSearchOpts : Bool -> Bool -> Maybe RecData -> Nat -> Bool -> Bool -> Bool -> Bool -> Bool -> Maybe (SearchOpts -> Name -> Nat -> ClosedTerm -> Core (Search (FC, List ImpClause))) -> SearchOpts

Projections:

.depth : SearchOpts -> Nat

.doneSplit : SearchOpts -> Bool

.genExpr : SearchOpts -> Maybe (SearchOpts -> Name -> Nat -> ClosedTerm -> Core (Search (FC, List ImpClause)))

.getRecData : SearchOpts -> Bool

.holesOK : SearchOpts -> Bool

.inArg : SearchOpts -> Bool

.inUnwrap : SearchOpts -> Bool

.ltor : SearchOpts -> Bool

.mustSplit : SearchOpts -> Bool

.recData : SearchOpts -> Maybe RecData

.holesOK : SearchOpts -> Bool

Visibility: public export

holesOK : SearchOpts -> Bool

Visibility: public export

.getRecData : SearchOpts -> Bool

Visibility: public export

getRecData : SearchOpts -> Bool

Visibility: public export

.recData : SearchOpts -> Maybe RecData

Visibility: public export

recData : SearchOpts -> Maybe RecData

Visibility: public export

.depth : SearchOpts -> Nat

Visibility: public export

depth : SearchOpts -> Nat

Visibility: public export

.inArg : SearchOpts -> Bool

Visibility: public export

inArg : SearchOpts -> Bool

Visibility: public export

.inUnwrap : SearchOpts -> Bool

Visibility: public export

inUnwrap : SearchOpts -> Bool

Visibility: public export

.ltor : SearchOpts -> Bool

Visibility: public export

ltor : SearchOpts -> Bool

Visibility: public export

.mustSplit : SearchOpts -> Bool

Visibility: public export

mustSplit : SearchOpts -> Bool

Visibility: public export

.doneSplit : SearchOpts -> Bool

Visibility: public export

doneSplit : SearchOpts -> Bool

Visibility: public export

.genExpr : SearchOpts -> Maybe (SearchOpts -> Name -> Nat -> ClosedTerm -> Core (Search (FC, List ImpClause)))

Visibility: public export

genExpr : SearchOpts -> Maybe (SearchOpts -> Name -> Nat -> ClosedTerm -> Core (Search (FC, List ImpClause)))

Visibility: public export

initSearchOpts : Bool -> Nat -> SearchOpts

Visibility: export

trySearch : Ref Ctxt Defs => Ref UST UState => Core (Search a) -> Core (Search a) -> Core (Search a)

Visibility: export

combine : Ref Ctxt Defs => Ref UST UState => (a -> b -> t) -> Search a -> Search b -> Core (Search t)

Visibility: export

exprSearchOpts : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => SearchOpts -> FC -> Name -> List Name -> Core (Search RawImp)

Visibility: export

exprSearch : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => FC -> Name -> List Name -> Core (Search RawImp)

Visibility: export

exprSearchN : Ref Ctxt Defs => Ref MD Metadata => Ref UST UState => Ref Syn SyntaxInfo => Ref ROpts REPLOpts => FC -> Nat -> Name -> List Name -> Core (List RawImp)

Visibility: export