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: Feb 06 2023 at 12:04 UTC