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?

Tried `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.

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: Jun 15 2024 at 08:01 UTC