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: Jun 25 2024 at 17:02 UTC