Core.Value

Definitions

data EvalOrder : Type

Totality: total
Visibility: public export
Constructors:

CBV : EvalOrder

CBN : EvalOrder

record EvalOpts : Type

Totality: total
Visibility: public export
Constructor: 

MkEvalOpts : Bool -> Bool -> Bool -> Bool -> Bool -> Maybe Nat -> List (Name, Nat) -> EvalOrder -> EvalOpts

Projections:

.argHolesOnly : EvalOpts -> Bool

.evalAll : EvalOpts -> Bool

.fuel : EvalOpts -> Maybe Nat

.holesOnly : EvalOpts -> Bool

.reduceLimit : EvalOpts -> List (Name, Nat)

.removeAs : EvalOpts -> Bool

.strategy : EvalOpts -> EvalOrder

.tcInline : EvalOpts -> Bool

.holesOnly : EvalOpts -> Bool

Visibility: public export

holesOnly : EvalOpts -> Bool

Visibility: public export

.argHolesOnly : EvalOpts -> Bool

Visibility: public export

argHolesOnly : EvalOpts -> Bool

Visibility: public export

.removeAs : EvalOpts -> Bool

Visibility: public export

removeAs : EvalOpts -> Bool

Visibility: public export

.evalAll : EvalOpts -> Bool

Visibility: public export

evalAll : EvalOpts -> Bool

Visibility: public export

.tcInline : EvalOpts -> Bool

Visibility: public export

tcInline : EvalOpts -> Bool

Visibility: public export

.fuel : EvalOpts -> Maybe Nat

Visibility: public export

fuel : EvalOpts -> Maybe Nat

Visibility: public export

.reduceLimit : EvalOpts -> List (Name, Nat)

Visibility: public export

reduceLimit : EvalOpts -> List (Name, Nat)

Visibility: public export

.strategy : EvalOpts -> EvalOrder

Visibility: public export

strategy : EvalOpts -> EvalOrder

Visibility: public export

defaultOpts : EvalOpts

Visibility: export

withHoles : EvalOpts

Visibility: export

withAll : EvalOpts

Visibility: export

withArgHoles : EvalOpts

Visibility: export

tcOnly : EvalOpts

Visibility: export

onLHS : EvalOpts

Visibility: export

cbn : EvalOpts

Visibility: export

cbv : EvalOpts

Visibility: export

LocalEnv : Scope -> Scope -> Type

Visibility: public export

data Closure : Scoped

Totality: total
Visibility: public export
Constructors:

MkClosure : EvalOpts -> LocalEnv free vars -> Env Term free -> Term (addInner free vars) -> Closure free

MkNFClosure : EvalOpts -> Env Term free -> NF free -> Closure free

Hints:

Convert Closure

Quote Closure

Show (Closure free)

Unify Closure

data NHead : Scoped

Totality: total
Visibility: public export
Constructors:

NLocal : Maybe Bool -> (idx : Nat) -> (0 _ : IsVar nm idx vars) -> NHead vars

NRef : NameType -> Name -> NHead vars

NMeta : Name -> Int -> List (Closure vars) -> NHead vars

Hints:

HasNames (NHead free)

Show (NHead free)

data NF : Scoped

Totality: not strictly positive
Visibility: public export
Constructors:

NBind : FC -> Name -> Binder (Closure vars) -> (Defs -> Closure vars -> Core (NF vars)) -> NF vars

NApp : FC -> NHead vars -> List (FC, Closure vars) -> NF vars

NDCon : FC -> Name -> Int -> Nat -> List (FC, Closure vars) -> NF vars

NTCon : FC -> Name -> Nat -> List (FC, Closure vars) -> NF vars

NAs : FC -> UseSide -> NF vars -> NF vars -> NF vars

NDelayed : FC -> LazyReason -> NF vars -> NF vars

NDelay : FC -> LazyReason -> Closure vars -> Closure vars -> NF vars

NForce : FC -> LazyReason -> NF vars -> List (FC, Closure vars) -> NF vars

NPrimVal : FC -> Constant -> NF vars

NErased : FC -> WhyErased (NF vars) -> NF vars

NType : FC -> Name -> NF vars

Hints:

Convert NF

HasNames (NF free)

Quote NF

Show (NF free)

Unify NF

ClosedClosure : Type

Visibility: public export

ClosedNF : Type

Visibility: public export

empty : LocalEnv free empty

Visibility: public export

ntCon : FC -> Name -> Nat -> List (FC, Closure vars) -> NF vars

Visibility: export

getLoc : NF vars -> FC

Visibility: export