eval_expr

Mathlib.Tactic.Eval

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.eval_expr

Lean4

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

As an example:
```lean
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`.
-/
@[term_parser 1000]
public meta def eval_expr : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Meta.eval_expr 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "eval% ") (ParserDescr.cat✝ `term 0))

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru