Is there a built-in notation to do exponentiation/power operation in coq? Like `2^3`

to get `8`

?

I found something like it at https://coq.inria.fr/library/Coq.Numbers.NatInt.NZLog.html but couldn't get it right.

see `pow`

and friends in the Definition index: https://coq.inria.fr/distrib/current/stdlib/index_definition_P.html - notations are usually given just after a definition.

The notation is generally `x^y`

as you already write, but sometimes one has to open some scope, e.g., `Z_scope`

for integers.

Last updated: Jan 31 2023 at 13:02 UTC