Derived evaluator instances for built-in Meta types

def Lean.Elab.ConfigEval.instEvalExprApplyNewGoals.evalExpr : Expr → MetaM Meta.ApplyNewGoals

Equations

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

def Lean.Elab.ConfigEval.instEvalTermApplyNewGoals.evalTerm : Term → TermElabM (Meta.ApplyNewGoals × Expr)

Equations

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

@[implicit_reducible]

instance Lean.Elab.ConfigEval.instEvalExprApplyNewGoals : EvalExpr Meta.ApplyNewGoals

Equations

• Lean.Elab.ConfigEval.instEvalExprApplyNewGoals = { evalExpr := Lean.Elab.ConfigEval.instEvalExprApplyNewGoals.evalExpr, expectedType? := some (Lean.Expr.const `Lean.Meta.ApplyNewGoals []) }

@[implicit_reducible]

instance Lean.Elab.ConfigEval.instEvalTermApplyNewGoals : EvalTerm Meta.ApplyNewGoals

Equations

• Lean.Elab.ConfigEval.instEvalTermApplyNewGoals = { evalTerm := Lean.Elab.ConfigEval.instEvalTermApplyNewGoals.evalTerm, typeExpr := Lean.Expr.const `Lean.Meta.ApplyNewGoals [] }

def Lean.Elab.ConfigEval.instEvalTermEtaStructMode.evalTerm : Term → TermElabM (Meta.EtaStructMode × Expr)

Equations

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

@[implicit_reducible]

instance Lean.Elab.ConfigEval.instEvalTermEtaStructMode : EvalTerm Meta.EtaStructMode

Equations

• Lean.Elab.ConfigEval.instEvalTermEtaStructMode = { evalTerm := Lean.Elab.ConfigEval.instEvalTermEtaStructMode.evalTerm, typeExpr := Lean.Expr.const `Lean.Meta.EtaStructMode [] }

def Lean.Elab.ConfigEval.instEvalExprEtaStructMode.evalExpr : Expr → MetaM Meta.EtaStructMode

Equations

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

@[implicit_reducible]

instance Lean.Elab.ConfigEval.instEvalExprEtaStructMode : EvalExpr Meta.EtaStructMode

Equations

• Lean.Elab.ConfigEval.instEvalExprEtaStructMode = { evalExpr := Lean.Elab.ConfigEval.instEvalExprEtaStructMode.evalExpr, expectedType? := some (Lean.Expr.const `Lean.Meta.EtaStructMode []) }

@[implicit_reducible]

instance Lean.Elab.ConfigEval.instEvalTermTransparencyMode : EvalTerm Meta.TransparencyMode

Equations

• Lean.Elab.ConfigEval.instEvalTermTransparencyMode = { evalTerm := Lean.Elab.ConfigEval.instEvalTermTransparencyMode.evalTerm, typeExpr := Lean.Expr.const `Lean.Meta.TransparencyMode [] }

def Lean.Elab.ConfigEval.instEvalExprTransparencyMode.evalExpr : Expr → MetaM Meta.TransparencyMode

Equations

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

@[implicit_reducible]

instance Lean.Elab.ConfigEval.instEvalExprTransparencyMode : EvalExpr Meta.TransparencyMode

Equations

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

def Lean.Elab.ConfigEval.instEvalTermTransparencyMode.evalTerm : Term → TermElabM (Meta.TransparencyMode × Expr)

Equations

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

@[implicit_reducible]

instance Lean.Elab.ConfigEval.instEvalTermOccurrences : EvalTerm Meta.Occurrences

Equations

• Lean.Elab.ConfigEval.instEvalTermOccurrences = { evalTerm := Lean.Elab.ConfigEval.instEvalTermOccurrences.evalTerm, typeExpr := Lean.Expr.const `Lean.Meta.Occurrences [] }

def Lean.Elab.ConfigEval.instEvalTermOccurrences.evalTerm : Term → TermElabM (Meta.Occurrences × Expr)

Equations

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

@[implicit_reducible]

instance Lean.Elab.ConfigEval.instEvalExprOccurrences : EvalExpr Meta.Occurrences

Equations

• Lean.Elab.ConfigEval.instEvalExprOccurrences = { evalExpr := Lean.Elab.ConfigEval.instEvalExprOccurrences.evalExpr, expectedType? := some (Lean.Expr.const `Lean.Meta.Occurrences []) }

def Lean.Elab.ConfigEval.instEvalExprOccurrences.evalExpr : Expr → MetaM Meta.Occurrences

Equations

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