Core.SchemeEval.Evaluate

Definitions

data SObj : Scoped

Totality: total
Visibility: public export
Constructor: 

MkSObj : ForeignObj -> SchVars vars -> SObj vars

data SHead : Scoped

Totality: total
Visibility: public export
Constructors:

SLocal : (idx : Nat) -> (0 _ : IsVar nm idx vars) -> SHead vars

SRef : NameType -> Name -> SHead vars

SMeta : Name -> Int -> List (Core (SNF vars)) -> SHead vars

data SNF : Scoped

Totality: total
Visibility: public export
Constructors:

SBind : FC -> Name -> Binder (SNF vars) -> (SObj vars -> Core (SNF vars)) -> SNF vars

SApp : FC -> SHead vars -> List (Core (SNF vars)) -> SNF vars

SDCon : FC -> Name -> Int -> Nat -> List (Core (SNF vars)) -> SNF vars

STCon : FC -> Name -> Nat -> List (Core (SNF vars)) -> SNF vars

SDelayed : FC -> LazyReason -> SNF vars -> SNF vars

SDelay : FC -> LazyReason -> Core (SNF vars) -> Core (SNF vars) -> SNF vars

SForce : FC -> LazyReason -> SNF vars -> SNF vars

SPrimVal : FC -> Constant -> SNF vars

SErased : FC -> WhyErased (SNF vars) -> SNF vars

SType : FC -> Name -> SNF vars

seval : Ref Ctxt Defs => SchemeMode -> Env Term vars -> Term vars -> Core (SObj vars)

Visibility: export

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

Visibility: export

toSNF : Ref Ctxt Defs => SObj vars -> Core (SNF vars)

Visibility: export