Idrall.Value

Definitions

Ty : Type

Visibility: public export

data Value : Type

Totality: not strictly positive
Visibility: public export
Constructors:

VConst : FC -> U -> Value

VVar : FC -> Name -> Int -> Value

VPrimVar : FC -> Value

VApp : FC -> Value -> Value -> Value

VLambda : FC -> Ty -> Closure -> Value

VHLam : FC -> HLamInfo -> (Value -> Either Error Value) -> Value

VPi : FC -> Ty -> Closure -> Value

VHPi : FC -> Name -> Value -> (Value -> Either Error Value) -> Value

VBool : FC -> Value

VBoolLit : FC -> Bool -> Value

VBoolAnd : FC -> Value -> Value -> Value

VBoolOr : FC -> Value -> Value -> Value

VBoolEQ : FC -> Value -> Value -> Value

VBoolNE : FC -> Value -> Value -> Value

VBoolIf : FC -> Value -> Value -> Value -> Value

VNatural : FC -> Value

VNaturalLit : FC -> Nat -> Value

VNaturalBuild : FC -> Value -> Value

VNaturalFold : FC -> Value -> Value -> Value -> Value -> Value

VNaturalIsZero : FC -> Value -> Value

VNaturalEven : FC -> Value -> Value

VNaturalOdd : FC -> Value -> Value

VNaturalSubtract : FC -> Value -> Value -> Value

VNaturalShow : FC -> Value -> Value

VNaturalToInteger : FC -> Value -> Value

VNaturalPlus : FC -> Value -> Value -> Value

VNaturalTimes : FC -> Value -> Value -> Value

VInteger : FC -> Value

VIntegerLit : FC -> Integer -> Value

VIntegerShow : FC -> Value -> Value

VIntegerNegate : FC -> Value -> Value

VIntegerClamp : FC -> Value -> Value

VIntegerToDouble : FC -> Value -> Value

VDouble : FC -> Value

VDoubleLit : FC -> Double -> Value

VDoubleShow : FC -> Value -> Value

VText : FC -> Value

VTextLit : FC -> VChunks -> Value

VTextAppend : FC -> Value -> Value -> Value

VTextShow : FC -> Value -> Value

VTextReplace : FC -> Value -> Value -> Value -> Value

VList : FC -> Ty -> Value

VListLit : FC -> Maybe Ty -> List Value -> Value

VListAppend : FC -> Value -> Value -> Value

VListBuild : FC -> Value -> Value -> Value

VListFold : FC -> Value -> Value -> Value -> Value -> Value -> Value

VListLength : FC -> Value -> Value -> Value

VListHead : FC -> Value -> Value -> Value

VListLast : FC -> Value -> Value -> Value

VListIndexed : FC -> Value -> Value -> Value

VListReverse : FC -> Value -> Value -> Value

VOptional : FC -> Ty -> Value

VNone : FC -> Ty -> Value

VSome : FC -> Ty -> Value

VEquivalent : FC -> Value -> Value -> Value

VAssert : FC -> Value -> Value

VRecord : FC -> SortedMap FieldName Value -> Value

VRecordLit : FC -> SortedMap FieldName Value -> Value

VUnion : FC -> SortedMap FieldName (Maybe Value) -> Value

VField : FC -> Value -> FieldName -> Value

VCombine : FC -> Value -> Value -> Value

VCombineTypes : FC -> Value -> Value -> Value

VPrefer : FC -> Value -> Value -> Value

VMerge : FC -> Value -> Value -> Maybe Value -> Value

VToMap : FC -> Value -> Maybe Value -> Value

VInject : FC -> SortedMap FieldName (Maybe Value) -> FieldName -> Maybe Value -> Value

VProject : FC -> Value -> Either (List FieldName) Value -> Value

VWith : FC -> Value -> List1 FieldName -> Value -> Value

Hints:

HasFC Value

Show Value

data Env : Type

Totality: total
Visibility: public export
Constructors:

Empty : Env

Skip : Env -> Name -> Env

Extend : Env -> Name -> Value -> Env

Hint: 

Show Env

data VChunks : Type

Totality: total
Visibility: public export
Constructor: 

MkVChunks : List (String, Value) -> String -> VChunks

Hints:

Monoid VChunks

Semigroup VChunks

Show VChunks

record Closure : Type

Totality: total
Visibility: public export
Constructor: 

MkClosure : Name -> Env -> Expr Void -> Closure

Projections:

.closureBody : Closure -> Expr Void

.closureEnv : Closure -> Env

.closureName : Closure -> Name

Hint: 

Show Closure

.closureName : Closure -> Name

Visibility: public export

closureName : Closure -> Name

Visibility: public export

.closureEnv : Closure -> Env

Visibility: public export

closureEnv : Closure -> Env

Visibility: public export

.closureBody : Closure -> Expr Void

Visibility: public export

closureBody : Closure -> Expr Void

Visibility: public export

data HLamInfo : Type

Totality: total
Visibility: public export
Constructors:

Prim : HLamInfo

Typed : String -> Value -> HLamInfo

NaturalSubtractZero : HLamInfo

Hint: 

Show HLamInfo

vFun : Value -> Value -> Value

  Returns `VHPi "_" a (\_ => Right b)`
  Non-dependent function arrow

Visibility: public export

VPrim : (Value -> Either Error Value) -> Value

  Returns `VHLam Prim f`

Visibility: public export