Stream: Coq users

Topic: Equations in sub-expressions


view this post on Zulip spaceloop (Oct 30 2020 at 00:55):

By using Equations I can define functions on the top-level nicely. Is there also syntax to use equations instead of the usual match construct? that is, can I use equations in a sub-expression, for example in the body of a lambda function?


Last updated: Jan 31 2023 at 12:01 UTC