Stream: general

Topic: definitional equality

Koundinya Vajjha (May 23 2019 at 14:51):

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 (May 23 2019 at 15:06):

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 (May 23 2019 at 15:20):

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

Koundinya Vajjha (May 23 2019 at 15:23):

ah. succeeds seems to do the trick. thanks!

Last updated: May 17 2021 at 21:12 UTC