In Haskell, we can use
$ to avoid too many parenthesis like
add 2 $ add 4 $ add 2 3
add 2 (add 4 (add 2 3))
Was wondering if there is something similar in coq?
Search ( (_ -> _) -> _ -> _). but could identify one. Or should the search pattern have been different?
Thanks. Didn't realize it was that simple.
Julin S has marked this topic as resolved.
if you want Coq to be like Haskell, I recommend carefully studying these:
That is useful but beware $ notations break scope inference.
N.to_nat (2 + n) works and
N.to_nat $ (2 + n)%N, but
N.to_nat $ 2 + n doesn't
Last updated: Sep 30 2023 at 06:01 UTC