Documentation

Mathlib.Tactic.Eval

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.

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
Instances For

    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.

    Instances For