Evaluator instances for built-in types

Some of these instances are hand-written instead of being derived, since the syntax may be special, or they might make special assumptions on the type (e.g. for Bool, we assume the identifiers true and false always refer to Bool's constructors).

EvalTerm instances

def Lean.Elab.ConfigEval.EvalTerm.evalBoolStx : Term → TermElabM (Bool × Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalTerm.evalNatStx : Term → TermElabM (Nat × Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalTerm.evalIntStx : Term → TermElabM (Int × Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalTerm.evalStringStx : Term → TermElabM (String × Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalTerm.evalNameStx : Term → TermElabM (Name × Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalTerm.evalOptionStx {α : Type} (typeExpr : Expr) (ev : Term → TermElabM (α × Expr)) : Term → TermElabM (Option α × Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalTerm.evalListStx {α : Type} (typeExpr : Expr) (ev : Term → TermElabM (α × Expr)) : Term → TermElabM (List α × Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalTerm.evalArrayStx {α : Type} (typeExpr : Expr) (ev : Term → TermElabM (α × Expr)) : Term → TermElabM (Array α × Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalTerm.evalProdStx {α α' : Type} (typeExpr typeExpr' : Expr) (ev : Term → TermElabM (α × Expr)) (ev' : Term → TermElabM (α' × Expr)) : Term → TermElabM ((α × α') × Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalTerm.evalDataValueStx (stx : Term) : TermElabM (DataValue × Expr)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalTerm.instBool : EvalTerm Bool

Equations

• Lean.Elab.ConfigEval.EvalTerm.instBool = { evalTerm := Lean.Elab.ConfigEval.EvalTerm.evalBoolStx, typeExpr := Lean.toTypeExpr Bool }

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalTerm.instNat : EvalTerm Nat

Equations

• Lean.Elab.ConfigEval.EvalTerm.instNat = { evalTerm := Lean.Elab.ConfigEval.EvalTerm.evalNatStx, typeExpr := Lean.toTypeExpr Nat }

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalTerm.instInt : EvalTerm Int

Equations

• Lean.Elab.ConfigEval.EvalTerm.instInt = { evalTerm := Lean.Elab.ConfigEval.EvalTerm.evalIntStx, typeExpr := Lean.toTypeExpr Int }

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalTerm.instString : EvalTerm String

Equations

• Lean.Elab.ConfigEval.EvalTerm.instString = { evalTerm := Lean.Elab.ConfigEval.EvalTerm.evalStringStx, typeExpr := Lean.toTypeExpr String }

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalTerm.instName : EvalTerm Name

Equations

• Lean.Elab.ConfigEval.EvalTerm.instName = { evalTerm := Lean.Elab.ConfigEval.EvalTerm.evalNameStx, typeExpr := Lean.toTypeExpr Lean.Name }

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalTerm.instOption {α : Type} [EvalTerm α] : EvalTerm (Option α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalTerm.instList {α : Type} [EvalTerm α] : EvalTerm (List α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalTerm.instArray {α : Type} [EvalTerm α] : EvalTerm (Array α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalTerm.instProd {α α' : Type} [EvalTerm α] [EvalTerm α'] : EvalTerm (α × α')

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalTerm.instDataValue : EvalTerm DataValue

Equations

• Lean.Elab.ConfigEval.EvalTerm.instDataValue = { evalTerm := Lean.Elab.ConfigEval.EvalTerm.evalDataValueStx, typeExpr := Lean.Expr.const `Lean.DataValue [] }

EvalExpr instances

def Lean.Elab.ConfigEval.EvalExpr.evalBoolExprCore (e : Expr) : MetaM Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalExpr.evalBoolExpr : Expr → MetaM Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalExpr.evalNatExprCore (e : Expr) : MetaM Nat

Equations

• Lean.Elab.ConfigEval.EvalExpr.evalNatExprCore e = (e.nat? <|> e.rawNatLit?).getDM Lean.Elab.ConfigEval.throwUnsupportedExpr

def Lean.Elab.ConfigEval.EvalExpr.evalNatExpr : Expr → MetaM Nat

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalExpr.evalIntExprCore (e : Expr) : MetaM Int

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalExpr.evalIntExpr : Expr → MetaM Int

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalExpr.evalStringExprCore : Expr → MetaM String

Equations

• Lean.Elab.ConfigEval.EvalExpr.evalStringExprCore (Lean.Expr.lit (Lean.Literal.strVal s)) = pure s
• Lean.Elab.ConfigEval.EvalExpr.evalStringExprCore x✝ = Lean.Elab.ConfigEval.throwUnsupportedExpr

def Lean.Elab.ConfigEval.EvalExpr.evalStringExpr : Expr → MetaM String

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalExpr.evalNameExprCore (e : Expr) : MetaM Name

Equations

• Lean.Elab.ConfigEval.EvalExpr.evalNameExprCore e = e.name?.getDM Lean.Elab.ConfigEval.throwUnsupportedExpr

def Lean.Elab.ConfigEval.EvalExpr.evalNameExpr : Expr → MetaM Name

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalExpr.evalOptionExprCore {α : Type} (ev : Expr → MetaM α) (e : Expr) : MetaM (Option α)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalExpr.evalOptionExpr {α : Type} (ev : Expr → MetaM α) (e : Expr) : MetaM (Option α)

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Elab.ConfigEval.EvalExpr.evalListExpr {α : Type} (ev : Expr → MetaM α) (e : Expr) (didWHNF : Bool := false) : MetaM (List α)

def Lean.Elab.ConfigEval.EvalExpr.evalArrayExpr {α : Type} (ev : Expr → MetaM α) : Expr → MetaM (Array α)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalExpr.evalDataValueExprCore (e : Expr) : MetaM DataValue

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.ConfigEval.EvalExpr.evalDataValueExpr : Expr → MetaM DataValue

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalExpr.instBool : EvalExpr Bool

Equations

• Lean.Elab.ConfigEval.EvalExpr.instBool = { evalExpr := Lean.Elab.ConfigEval.EvalExpr.evalBoolExpr, expectedType? := some (Lean.toTypeExpr Bool) }

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalExpr.instNat : EvalExpr Nat

Equations

• Lean.Elab.ConfigEval.EvalExpr.instNat = { evalExpr := Lean.Elab.ConfigEval.EvalExpr.evalNatExpr, expectedType? := some (Lean.toTypeExpr Nat) }

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalExpr.instInt : EvalExpr Int

Equations

• Lean.Elab.ConfigEval.EvalExpr.instInt = { evalExpr := Lean.Elab.ConfigEval.EvalExpr.evalIntExpr, expectedType? := some (Lean.toTypeExpr Int) }

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalExpr.instString : EvalExpr String

Equations

• Lean.Elab.ConfigEval.EvalExpr.instString = { evalExpr := Lean.Elab.ConfigEval.EvalExpr.evalStringExpr, expectedType? := some (Lean.toTypeExpr String) }

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalExpr.instName : EvalExpr Name

Equations

• Lean.Elab.ConfigEval.EvalExpr.instName = { evalExpr := Lean.Elab.ConfigEval.EvalExpr.evalNameExpr, expectedType? := some (Lean.toTypeExpr Lean.Name) }

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalExpr.instOption {α : Type} [EvalExpr α] : EvalExpr (Option α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalExpr.instList {α : Type} [EvalExpr α] : EvalExpr (List α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalExpr.instArray {α : Type} [EvalExpr α] : EvalExpr (Array α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Elab.ConfigEval.EvalExpr.instDataValue : EvalExpr DataValue

Equations

• Lean.Elab.ConfigEval.EvalExpr.instDataValue = { evalExpr := Lean.Elab.ConfigEval.EvalExpr.evalDataValueExpr, expectedType? := none }