Stream: Coq users

Topic: ✔ I forgot how to tell Coq that two types are equal

Lessness (Jul 15 2022 at 19:53):

Structure test A B (H: A = B) := {
  t: forall (x: A) (y: B), x = y
}.

Let's use this as toy example. How to tell Coq that A = B and therefore x = y makes sense?

Lessness (Jul 15 2022 at 19:58):

Solved.

Structure test A B (H: A = B) := {
  t: forall (x: A) (y: B), eq_rect _ _ x _ H = y
}.

Notification Bot (Jul 15 2022 at 19:58):

Lessness has marked this topic as resolved.

Joshua Grosso (Jul 15 2022 at 20:00):

There's also the rew notation, which imo looks nice here:

Import EqNotations.

Structure test A B (H: A = B) := {
  t: forall (x: A) (y: B), rew H in x = y
}.

Last updated: Apr 16 2024 at 09:01 UTC