Zulip Chat Archive

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 :=

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: Aug 03 2023 at 10:10 UTC