def Units.formatExp (e : String) (n : Rat) : String

Equations

• Units.formatExp e { num := Int.ofNat 1, den_nz := ⋯, reduced := ⋯ } = e
• Units.formatExp e { num := Int.ofNat 2, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "²"
• Units.formatExp e { num := Int.ofNat 3, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "³"
• Units.formatExp e { num := Int.ofNat 4, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "⁴"
• Units.formatExp e { num := Int.ofNat 5, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "⁵"
• Units.formatExp e { num := Int.ofNat 6, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "⁶"
• Units.formatExp e { num := Int.ofNat 7, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "⁷"
• Units.formatExp e { num := Int.ofNat 8, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "⁸"
• Units.formatExp e { num := Int.ofNat 9, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "⁹"
• Units.formatExp e { num := Int.negSucc 0, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "⁻¹"
• Units.formatExp e { num := Int.negSucc 1, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "⁻²"
• Units.formatExp e { num := Int.negSucc 2, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "⁻³"
• Units.formatExp e { num := Int.negSucc 3, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "⁻⁴"
• Units.formatExp e { num := Int.negSucc 4, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "⁻⁵"
• Units.formatExp e { num := Int.negSucc 5, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "⁻⁶"
• Units.formatExp e { num := Int.negSucc 6, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "⁻⁷"
• Units.formatExp e { num := Int.negSucc 7, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "⁻⁸"
• Units.formatExp e { num := Int.negSucc 8, den_nz := ⋯, reduced := ⋯ } = toString e ++ toString "⁻⁹"
• Units.formatExp e n = toString e ++ toString "^" ++ toString n