Is there a built-in notation to do exponentiation/power operation in coq? Like
2^3 to get
I found something like it at https://coq.inria.fr/library/Coq.Numbers.NatInt.NZLog.html but couldn't get it right.
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: Sep 28 2023 at 11:01 UTC