Yoav Cohen (Jul 22 2026 at 10:38): Yoav Cohen (Jul 22 2026 at 10:38):
What even is the difference between those instances such that I need to like
fix a :: 'b
in the second one or whatever.
Mathias Fleury (Jul 22 2026 at 18:16):the types to infer are "deferred" to the next line
Mathias Fleury (Jul 22 2026 at 18:17):in a = a, you have no restriction, so you end up with type 'b, while in the first case F a restricts a to be exactly the right type
Yoav Cohen (Jul 22 2026 at 18:33):I don't understand. what kinda restriction does F a put on a's type?
Mathias Fleury (Jul 23 2026 at 19:58):F has a type due to the lemma
Mathias Fleury (Jul 23 2026 at 19:59):the type is inferred there
Last updated: Aug 11 2026 at 20:46 UTC