Structures · Lean core

HomogeneousPow

The completely homogeneous version of Pow where the exponent has the same type as the base. The purpose of this class is that it provides a default Pow instance, which can be used to specialize the exponent to have the same type as the base's type during elaboration. This is to say, a type should provide an instance for this class in case x ^ y should be elaborated with both x and y having the same type. For example, the Float type provides an instance of this class, which causes expressions such as (2.2 ^ 2.2 : Float) to elaborate.

Defined in

Init.Prelude

Shape

One type argument · adds pow