# \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.

- In this case,