Stream: Coq users

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

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?

Julin S (Jan 05 2022 at 05:47):

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

Karl Palmskog (Jan 05 2022 at 07:59):

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

Julin S (Jan 05 2022 at 08:32):

Thanks. Didn't realize it was that simple.

Notification Bot (Jan 05 2022 at 08:32):

Julin S has marked this topic as resolved.

Karl Palmskog (Jan 05 2022 at 08:35):

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

• https://github.com/jwiegley/coq-haskell
• https://github.com/plclub/hs-to-coq

Paolo Giarrusso (Jan 05 2022 at 12:17):

That is useful but beware $ notations break scope inference.

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: Apr 18 2024 at 23:01 UTC