Zulip Chat Archive

Stream: general

Topic: definitional equality


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Koundinya Vajjha (May 23 2019 at 15:20):

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

view this post on Zulip 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