Stream: Coq users

Topic: Exponentiation / power operator in coq


view this post on Zulip Julin S (Nov 19 2021 at 13:06):

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.

view this post on Zulip Karl Palmskog (Nov 19 2021 at 13:21):

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