class Units.DPow (α : Type u) (β : Type v) (γ : outParam (β → Type w)) : Type (max (max u v) w)

Dependent power operator, allows to have the output type depend on the exponent. q ^ᵈ n:

• if n : ℕ uses q.npow
• if n : ℤ uses q.zpow
• if n : ℚ uses q.qpow

Examples:

• q ^ᵈ 2 -- npow
• q ^ᵈ (-2 : ℤ) -- zpow
• q ^ᵈ (1/3 : ℚ) -- qpow

• pow : α → (n : β) → γ n

def Units.«term_^ᵈ_» : Lean.TrailingParserDescr

Equations

• Units.«term_^ᵈ_» = Lean.ParserDescr.trailingNode `Units.«term_^ᵈ_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^ᵈ ") (Lean.ParserDescr.cat `term 80))