Stream: Coq users

Topic: ✔ Is there a way to avoid too many parenthesis?


view this post on Zulip Julin S (Jan 05 2022 at 05:40):

In Haskell, we can use $ to avoid too many parenthesis like

add 2 $ add 4 $ add 2 3

instead of

add 2 (add 4 (add 2 3))

Was wondering if there is something similar in coq?

view this post on Zulip Julin S (Jan 05 2022 at 05:47):

Tried Search ( (_ -> _) -> _ -> _). but could identify one. Or should the search pattern have been different?

view this post on Zulip Karl Palmskog (Jan 05 2022 at 07:59):

https://github.com/jwiegley/coq-haskell/blob/a6baf6e2f53e53ee91bbfc8904b718ef90bf5c6b/src/Prelude.v#L21

view this post on Zulip Julin S (Jan 05 2022 at 08:32):

Thanks. Didn't realize it was that simple.

view this post on Zulip Notification Bot (Jan 05 2022 at 08:32):

Julin S has marked this topic as resolved.

view this post on Zulip Karl Palmskog (Jan 05 2022 at 08:35):

if you want Coq to be like Haskell, I recommend carefully studying these:

view this post on Zulip Paolo Giarrusso (Jan 05 2022 at 12:17):

That is useful but beware $ notations break scope inference.

view this post on Zulip Paolo Giarrusso (Jan 05 2022 at 12:20):

So eg N.to_nat (2 + n) works and N.to_nat $ (2 + n)%N, but N.to_nat $ 2 + n doesn't


Last updated: Jan 28 2023 at 06:30 UTC