import Mathlib.Algebra.Group.Nat

namespace String

def 
fillLeft: String → Char → ℕ → String
fillLeft (
s: String
s : 
String: Type
String) (
c: Char
c : 
Char: Type
Char) (
n: ℕ
n : 
Nat: Type
Nat)  : 
String: Type
String :=
  
"": String
"".
pushn: String → Char → ℕ → String
pushn 
c: Char
c (
n: ℕ
n - 
s: String
s.
length: String → ℕ
length) ++ 
s: String
s

end String

namespace Float

def 
intPart: Float → String
intPart (
f: Float
f : 
Float: Type
Float) : 
String: Type
String :=
  
String.join: List String → String
String.join <| 
f: Float
f.
toString: Float → String
toString.
splitOn: String → optParam String " " → List String
splitOn 
".": String
"." |>.
take: {α : Type} → ℕ → List α → List α
take 
1: ℕ
1

def 
toDecimal: Float → ℕ → String
toDecimal (
f: Float
f : 
Float: Type
Float) (
precision: ℕ
precision : 
Nat: Type
Nat) : 
String: Type
String :=
  let 
int: Float
int := 
f: Float
f.
round: Float → Float
round
  let 
intStr: String
intStr := 
int: Float
int.
intPart: Float → String
intPart
  let 
fraction: Float
fraction := ((
f: Float
f-
int: Float
int) * (
10: ℕ
10 ^ 
precision: ℕ
precision).
toFloat: ℕ → Float
toFloat).
abs: Float → Float
abs.
round: Float → Float
round
  let 
fractionStr: String
fractionStr := 
fraction: Float
fraction.
intPart: Float → String
intPart.
fillLeft: String → Char → ℕ → String
fillLeft 
'0': Char
'0' 
precision: ℕ
precision
  if 
precision: ℕ
precision > 
0: ℕ
0 then s!"{
intStr: String
intStr}.{
fractionStr: String
fractionStr}" else 
intStr: String
intStr

end Float

info: "3.11235"

#guard_msgs
Error: ❌ Docstring on `#guard_msgs` does not match generated message:

info: "3.11235" in
#eval
"3.11235"
 
3.1123456: Float
3.1123456.
toDecimal: Float → ℕ → String
toDecimal 
5: ℕ
5

info: "-123.4567890"

#guard_msgs
Error: ❌ Docstring on `#guard_msgs` does not match generated message:

info: "-123.4567890" in
#eval
"-123.4567890"
 (-
123.456789: Float
123.456789).
toDecimal: Float → ℕ → String
toDecimal 
7: ℕ
7

info: "0.0000100"

#guard_msgs
Error: ❌ Docstring on `#guard_msgs` does not match generated message:

info: "0.0000100" in
#eval
"0.0000100"
 (
0.00001: Float
0.00001).
toDecimal: Float → ℕ → String
toDecimal 
7: ℕ
7

info: "-0.3000000"

#guard_msgs
Error: ❌ Docstring on `#guard_msgs` does not match generated message:

info: "-0.3000000" in
#eval
"-0.3000000"
 (-
0.3: Float
0.3).
toDecimal: Float → ℕ → String
toDecimal 
7: ℕ
7

info: "-1"

#guard_msgs
Error: ❌ Docstring on `#guard_msgs` does not match generated message:

info: "-1" in
#eval
"-1"
 (-
1.23: Float
1.23).
toDecimal: Float → ℕ → String
toDecimal 
0: ℕ
0