Zulip Chat Archive
Stream: general
Topic: dependent type hell resolved by heq_of_eq_mp
Kenny Lau (Apr 12 2020 at 07:02):
heq_of_eq_mp resolved my dependent type hell
Kenny Lau (Apr 12 2020 at 07:02):
heq_of_eq_mp : ∀ {α β : Sort u_1} {a : α} {a' : β} (e : α = β), eq.mp e a = a' → a == a'
Last updated: May 02 2025 at 03:31 UTC