Core.Normalise

Reexports

Definitions

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

Visibility: export

glueBack : Ref Ctxt Defs => Defs -> Env Term vars -> NF vars -> Glued vars

Visibility: export

glueClosure : Ref Ctxt Defs => Defs -> Env Term vars -> Closure vars -> Glued vars

Visibility: export

normalise : Ref Ctxt Defs => Defs -> Env Term free -> Term free -> Core (Term free)

Visibility: export

normaliseOpts : Ref Ctxt Defs => EvalOpts -> Defs -> Env Term free -> Term free -> Core (Term free)

Visibility: export

normaliseHoles : Ref Ctxt Defs => Defs -> Env Term free -> Term free -> Core (Term free)

Visibility: export

normaliseLHS : Ref Ctxt Defs => Defs -> Env Term free -> Term free -> Core (Term free)

Visibility: export

tryNormaliseSizeLimit : Ref Ctxt Defs => Defs -> Nat -> Env Term free -> Term free -> Core (Term free)

Visibility: export

normaliseSizeLimit : Ref Ctxt Defs => Defs -> Nat -> Env Term free -> Term free -> Core (Term free)

Visibility: export

normaliseArgHoles : Ref Ctxt Defs => Defs -> Env Term free -> Term free -> Core (Term free)

Visibility: export

normaliseAll : Ref Ctxt Defs => Defs -> Env Term free -> Term free -> Core (Term free)

Visibility: export

normaliseScope : Ref Ctxt Defs => Defs -> Env Term free -> Term free -> Core (Term free)

Visibility: export

etaContract : Ref Ctxt Defs => Term vars -> Core (Term vars)

Visibility: export

getValArity : Defs -> Env Term vars -> NF vars -> Core Nat

Visibility: export

getArity : Ref Ctxt Defs => Defs -> Env Term vars -> Term vars -> Core Nat

Visibility: export

logNF : Ref Ctxt Defs => LogTopic -> Nat -> Lazy String -> Env Term vars -> NF vars -> Core ()

Visibility: export

logTermNF' : Ref Ctxt Defs => LogTopic -> Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()

Visibility: export

logTermNF : Ref Ctxt Defs => LogTopic -> Nat -> Lazy String -> Env Term vars -> Term vars -> Core ()

Visibility: export

logGlue : Ref Ctxt Defs => LogTopic -> Nat -> Lazy String -> Glued vars -> Core ()

Visibility: export

logGlueNF : Ref Ctxt Defs => LogTopic -> Nat -> Lazy String -> Env Term vars -> Glued vars -> Core ()

Visibility: export

logEnv : Ref Ctxt Defs => LogTopic -> Nat -> String -> Env Term vars -> Core ()

Visibility: export

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

Visibility: export

normalisePrims : Ref Ctxt Defs => (Constant -> Bool) -> (arg -> Maybe Constant) -> Bool -> List Name -> Name -> List arg -> Term vs -> Env Term vs -> Core (Maybe (Term vs))

Visibility: export