The eval% term elaborator

This file provides the eval% x term elaborator, which evaluates the constant x at compile-time in the interpreter, and interpolates it into the expression.

def Mathlib.Meta.eval_expr : Lean.ParserDescr

eval% x evaluates the term x : X in the interpreter, and then injects the resulting expression.

As an example:

example : 2^10 = eval% 2^10 := by
  -- goal is `2^10 = 1024`
  sorry

This only works if a Lean.ToExpr X instance is available.

Tip: you can use show_term eval% x to see the value of eval% x.

Equations

• Mathlib.Meta.eval_expr = Lean.ParserDescr.node `Mathlib.Meta.eval_expr 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "eval% ") (Lean.ParserDescr.cat `term 0))

unsafe def Mathlib.Meta.elabEvalExpr : Lean.Elab.Term.TermElab

eval% x evaluates the term x : X in the interpreter, and then injects the resulting expression.

As an example:

example : 2^10 = eval% 2^10 := by
  -- goal is `2^10 = 1024`
  sorry

This only works if a Lean.ToExpr X instance is available.

Tip: you can use show_term eval% x to see the value of eval% x.