let bindings in expr

Stream: general

[Frédéric Le Roux]

When a notation is introduced using the keyword let, the defining equation does not appear in the context.
I am also unable to get it from the local context when writing tactics. For instance, for the code

example (x: X) : true :=
begin
  let y:= x,
end

after the letexpression, the proof state contains two local constants xand y, but the equation y=xis somehow hidden...
When I analyze the expr coding for y, I would expect to find an elet term in the def of expr:

/- An explicit let binding. -/
| elet       (var_name : name) (type : expr) (assignment : expr) (body : expr) : expr

but this is not the case, I see no difference between xand y, they are both analyzed as local_const.

So my question is: how can I recover the hidden defining equation when writing tactics?

[Mario Carneiro]

it's not an equation, it is a special kind of variable declaration in the context (which is shown like y : X := x instead of just y : X)

[Mario Carneiro]

docs#tactic.local_def_value will tell you the value of a let-bound variable in the context

[Frédéric Le Roux]

Thank you!