Stream: Coq users

Topic: ✔ type inference in `let in` expression

view this post on Zulip Remzi Yang (Apr 20 2023 at 02:06):

Thank you @Ali Caglayan , that fixs my problem. BTW, why do we need to add ' before the (...),

view this post on Zulip Remzi Yang (Apr 20 2023 at 02:13):

Never I find it from the coq doc: https://coq.inria.fr/refman/language/extensions/match.html#second-destructuring-let-syntax
Thanks again @Ali Caglayan !

view this post on Zulip Notification Bot (Apr 20 2023 at 02:13):

Remzi Yang has marked this topic as resolved.

Last updated: Oct 04 2023 at 19:01 UTC