Core.Normalise.Eval

Definitions

data Glued : Scoped

Totality: possibly not terminating due to call to $resolved17792
Visibility: public export
Constructor: 

MkGlue : Bool -> Core (Term vars) -> (Ref Ctxt Defs -> Core (NF vars)) -> Glued vars

isFromTerm : Glued vars -> Bool

Visibility: export

getTerm : Glued vars -> Core (Term vars)

Visibility: export

getNF : Ref Ctxt Defs => Glued vars -> Core (NF vars)

Visibility: export

Stack : Scoped

Visibility: public export

evalClosure : Ref Ctxt Defs => Defs -> Closure free -> Core (NF free)

Visibility: export

evalArg : Ref Ctxt Defs => Defs -> Closure free -> Core (NF free)

Visibility: export

toClosure : EvalOpts -> Env Term outer -> Term outer -> Closure outer

Visibility: export

applyToStack : Defs -> EvalOpts -> Ref Ctxt Defs => Env Term free -> NF free -> Stack free -> Core (NF free)

Visibility: export

evalClosureWithOpts : Ref Ctxt Defs => Defs -> EvalOpts -> Closure free -> Core (NF free)

Visibility: export

nf : Ref Ctxt Defs => Defs -> Env Term vars -> Term vars -> Core (NF vars)

Visibility: export

nfOpts : Ref Ctxt Defs => EvalOpts -> Defs -> Env Term vars -> Term vars -> Core (NF vars)

Visibility: export

gnf : Env Term vars -> Term vars -> Glued vars

Visibility: export

gnfOpts : EvalOpts -> Env Term vars -> Term vars -> Glued vars

Visibility: export

gType : FC -> Name -> Glued vars

Visibility: export

gErased : FC -> Glued vars

Visibility: export

continueNF : Ref Ctxt Defs => Defs -> Env Term vars -> NF vars -> Core (NF vars)

Visibility: export