evaluating expressions within proofs

Stream: new members

[Arthur Paulino]

Is there a way to evaluate (and print) the value of a variable within the scope of a proof?

[Jason Rute]

Can you give a #mwe?

[Jason Rute]

And do you mean tactic proof or term proof?

[Scott Morrison]

Perhaps you mean doing the equivalent of #eval, but mid-way through a proof?

[Jason Rute]

Here are two examples. You may need to turn widgets off to see this. IIRC, there is a bug in widgets which doesn't show the := 1 in the examples below.

example (m n : ℕ) : m + n = n + m :=
let a := 1 in _  -- use _ to find the value of `a` in the local context of a term proof:
-- m n : ℕ,
-- a : ℕ := 1
-- ⊢ m + n = n + m

example (m n : ℕ) : let a := 1 in m + n = n + m :=
begin
  intro a,
  -- The goal should show you the value of `a` in the local context of a tactic proof.
  -- m n : ℕ,
  -- a : ℕ := 1
  -- ⊢ m + n = n + m
end

[Jason Rute]

This doesn't show you the values of assigned metavariables though. (Honestly, I'm not exactly sure what you're asking for.)