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 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: - 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: Jun 24 2024 at 00:02 UTC