Stream: Coq users

Topic: `f_equal` on data constructors?

view this post on Zulip Ignat Insarov (Jun 20 2021 at 15:48):

Is it healthy to apply f_equal in a context like this?

  ============================
  Some x = Some y

What is the appropriate tactic to pass to x = y?

view this post on Zulip Théo Winterhalter (Jun 20 2021 at 15:49):

I would also use the f_equal tactic here.

view this post on Zulip Ignat Insarov (Jun 20 2021 at 16:01):

Thanks!

Last updated: Oct 13 2024 at 01:02 UTC