definitional equality

Stream: general

[Koundinya Vajjha]

is there any way of listing all theexpr which are definitionally equal to a given expr?

here is a test example:

lemma test: ∀ x: ℕ, let y := x in x ≠ y :=
begin
intros,
sorry
end

I want a function all_def_eq which takes in y and spits out x.

[Rob Lewis]

You can use list.mfilter and tactic.is_def_eq to filter the local context for things that are defeq to a given expr.

[Koundinya Vajjha]

sorry, how do i make a boolean out of is_def_eq?

[Koundinya Vajjha]

ah. succeeds seems to do the trick. thanks!