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: Oct 13 2024 at 01:02 UTC