\module Function.Meta

$ and #

These metas are analogical to Haskell’s $ operator ($ is right-associative and # is left-associative), but they also work with implicit arguments.

Also, it’s also possible to define $ as a defined meta:

\meta \infixr 0 $ f a => f a

But then it won’t work with implicit arguments. In Haskell, you can apply $ partially (like $ a), and you can do this in Arend via implicit lambdas ( __ $ a).

repeat

There are two ways to invoke this meta:

  • repeat {n} f x – it reduces to x if n is 0 and repeat {x} f (f x) if n is suc x.
  • repeat f x – it tries to typecheck f x, and if it fails, return x, otherwise return f (repeat f x).
    • In this case, f has to be a meta.