feat: add Float.toFloat32 and Float32.toFloat32

src/Init/Data/Array/Lemmas.lean

@@ -19,6 +19,8 @@ import Init.Data.List.ToArray
 ## Theorems about `Array`.
 -/
 
+
+
 namespace Array
 
 /-! ## Preliminaries -/
@@ -182,14 +184,6 @@ theorem getElem_eq_getElem?_get (a : Array α) (i : Nat) (h : i < a.size) :
     a[i] = a[i]?.get (by simp [getElem?_eq_getElem, h]) := by
   simp [getElem_eq_iff]
 
-theorem getD_getElem? (a : Array α) (i : Nat) (d : α) :
-    a[i]?.getD d = if p : i < a.size then a[i]'p else d := by
-  if h : i < a.size then
-    simp [h, getElem?_def]
-  else
-    have p : i ≥ a.size := Nat.le_of_not_gt h
-    simp [getElem?_eq_none p, h]
-
 @[simp] theorem getElem?_empty {n : Nat} : (#[] : Array α)[n]? = none := rfl
 
 theorem getElem_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
@@ -716,164 +710,6 @@ theorem all_push [BEq α] {as : Array α} {a : α} {p : α → Bool} :
     (l.push a).contains b = (l.contains b || b == a) := by
   simp [contains]
 
-/-! ### set -/
-
-
-/-! # set -/
-
-@[simp] theorem getElem_set_self (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
-      (eq : i = j) (p : j < (a.set i v).size) :
-    (a.set i v)[j]'p = v := by
-  cases a
-  simp
-  simp [set, ← getElem_toList, ←eq]
-
-@[deprecated getElem_set_self (since := "2024-12-11")]
-abbrev getElem_set_eq := @getElem_set_self
-
-@[simp] theorem getElem?_set_self (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
-    (a.set i v)[i]? = v := by simp [getElem?_eq_getElem, h]
-
-@[deprecated getElem?_set_self (since := "2024-12-11")]
-abbrev getElem?_set_eq := @getElem?_set_self
-
-@[simp] theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
-    (pj : j < (a.set i v).size) (h : i ≠ j) :
-    (a.set i v)[j]'pj = a[j]'(size_set a i v _ ▸ pj) := by
-  simp only [set, ← getElem_toList, List.getElem_set_ne h]
-
-@[simp] theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
-    (ne : i ≠ j) : (a.set i v)[j]? = a[j]? := by
-  by_cases h : j < a.size <;> simp [getElem?_eq_getElem, getElem?_eq_none, Nat.ge_of_not_lt, ne, h]
-
-theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
-    (h : j < (a.set i v).size) :
-    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ ▸ h) := by
-  by_cases p : i = j <;> simp [p]
-
-theorem getElem?_set (a : Array α) (i : Nat) (h : i < a.size) (v : α) (j : Nat) :
-    (a.set i v)[j]? = if i = j then some v else a[j]? := by
-  split <;> simp_all
-
-@[simp] theorem set_getElem_self {as : Array α} {i : Nat} (h : i < as.size) :
-    as.set i as[i] = as := by
-  cases as
-  simp
-
-@[simp] theorem set_eq_empty_iff {as : Array α} (n : Nat) (a : α) (h) :
-     as.set n a = #[] ↔ as = #[] := by
-  cases as <;> cases n <;> simp [set]
-
-theorem set_comm (a b : α)
-    {n m : Nat} (as : Array α) {hn : n < as.size} {hm : m < (as.set n a).size} (h : n ≠ m) :
-    (as.set n a).set m b = (as.set m b (by simpa using hm)).set n a (by simpa using hn) := by
-  cases as
-  simp [List.set_comm _ _ _ h]
-
-@[simp]
-theorem set_set (a b : α) (as : Array α) (n : Nat) (h : n < as.size) :
-    (as.set n a).set n b (by simpa using h) = as.set n b := by
-  cases as
-  simp
-
-theorem mem_set (as : Array α) (n : Nat) (h : n < as.size) (a : α) :
-    a ∈ as.set n a := by
-  simp [mem_iff_getElem]
-  exact ⟨n, (by simpa using h), by simp⟩
-
-theorem mem_or_eq_of_mem_set
-    {as : Array α} {n : Nat} {a b : α} {w : n < as.size} (h : a ∈ as.set n b) : a ∈ as ∨ a = b := by
-  cases as
-  simpa using List.mem_or_eq_of_mem_set (by simpa using h)
-
-/-! # setIfInBounds -/
-
-@[simp] theorem set!_is_setIfInBounds : @set! = @setIfInBounds := rfl
-
-@[simp] theorem size_setIfInBounds (as : Array α) (index : Nat) (val : α) :
-    (as.setIfInBounds index val).size = as.size := by
-  if h : index < as.size  then
-    simp [setIfInBounds, h]
-  else
-    simp [setIfInBounds, h]
-
-theorem getElem_setIfInBounds (as : Array α) (i : Nat) (v : α) (j : Nat)
-    (hj : j < (as.setIfInBounds i v).size) :
-    (as.setIfInBounds i v)[j]'hj = if i = j then v else as[j]'(by simpa using hj) := by
-  simp only [setIfInBounds]
-  split
-  · simp [getElem_set]
-  · simp only [size_setIfInBounds] at hj
-    rw [if_neg]
-    omega
-
-@[simp] theorem getElem_setIfInBounds_self (as : Array α) {i : Nat} (v : α) (h : _) :
-    (as.setIfInBounds i v)[i]'h = v := by
-  simp at h
-  simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_self]
-
-@[deprecated getElem_setIfInBounds_self (since := "2024-12-11")]
-abbrev getElem_setIfInBounds_eq := @getElem_setIfInBounds_self
-
-@[simp] theorem getElem_setIfInBounds_ne (as : Array α) {i : Nat} (v : α) {j : Nat}
-    (hj : j < (as.setIfInBounds i v).size) (h : i ≠ j) :
-    (as.setIfInBounds i v)[j]'hj = as[j]'(by simpa using hj) := by
-  simp [getElem_setIfInBounds, h]
-
-@[simp]
-theorem getElem?_setIfInBounds_self (as : Array α) {i : Nat} (p : i < as.size) (v : α) :
-    (as.setIfInBounds i v)[i]? = some v := by
-  simp [getElem?_eq_getElem, p]
-
-@[deprecated getElem?_setIfInBounds_self (since := "2024-12-11")]
-abbrev getElem?_setIfInBounds_eq := @getElem?_setIfInBounds_self
-
-theorem getElem?_setIfInBounds {as : Array α} {i j : Nat} {a : α}  :
-    (as.setIfInBounds i a)[j]? = if i = j then if i < as.size then some a else none else as[j]? := by
-  cases as
-  simp [List.getElem?_set]
-
-@[simp] theorem getElem?_setIfInBounds_ne {as : Array α} {i j : Nat} (h : i ≠ j) {a : α}  :
-    (as.setIfInBounds i a)[j]? = as[j]? := by
-  simp [getElem?_setIfInBounds, h]
-
-theorem setIfInBounds_eq_of_size_le {l : Array α} {n : Nat} (h : l.size ≤ n) {a : α} :
-    l.setIfInBounds n a = l := by
-  cases l
-  simp [List.set_eq_of_length_le (by simpa using h)]
-
-@[simp] theorem setIfInBounds_eq_empty_iff {as : Array α} (n : Nat) (a : α) :
-     as.setIfInBounds n a = #[] ↔ as = #[] := by
-  cases as <;> cases n <;> simp
-
-theorem setIfInBounds_comm (a b : α)
-    {n m : Nat} (as : Array α) (h : n ≠ m) :
-    (as.setIfInBounds n a).setIfInBounds m b = (as.setIfInBounds m b).setIfInBounds n a := by
-  cases as
-  simp [List.set_comm _ _ _ h]
-
-@[simp]
-theorem setIfInBounds_setIfInBounds (a b : α) (as : Array α) (n : Nat) :
-    (as.setIfInBounds n a).setIfInBounds n b = as.setIfInBounds n b := by
-  cases as
-  simp
-
-theorem mem_setIfInBounds (as : Array α) (n : Nat) (h : n < as.size) (a : α) :
-    a ∈ as.setIfInBounds n a := by
-  simp [mem_iff_getElem]
-  exact ⟨n, (by simpa using h), by simp⟩
-
-theorem mem_or_eq_of_mem_setIfInBounds
-    {as : Array α} {n : Nat} {a b : α} (h : a ∈ as.setIfInBounds n b) : a ∈ as ∨ a = b := by
-  cases as
-  simpa using List.mem_or_eq_of_mem_set (by simpa using h)
-
-/-- Simplifies a normal form from `get!` -/
-@[simp] theorem getD_get?_setIfInBounds (a : Array α) (i : Nat) (v d : α) :
-    (setIfInBounds a i v)[i]?.getD d = if i < a.size then v else d := by
-  by_cases h : i < a.size <;>
-    simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_getElem?]
-
 theorem singleton_inj : #[a] = #[b] ↔ a = b := by
   simp
 
@@ -984,31 +820,102 @@ theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by si
 
 /-! # get -/
 
-@[deprecated getElem?_eq_getElem (since := "2024-12-11")]
 theorem getElem?_lt
     (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i] := dif_pos h
 
-@[deprecated getElem?_eq_none (since := "2024-12-11")]
 theorem getElem?_ge
     (a : Array α) {i : Nat} (h : i ≥ a.size) : a[i]? = none := dif_neg (Nat.not_lt_of_le h)
 
 @[simp] theorem get?_eq_getElem? (a : Array α) (i : Nat) : a.get? i = a[i]? := rfl
 
-@[deprecated getElem?_eq_none (since := "2024-12-11")]
 theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = none := by
-  simp [getElem?_eq_none, h]
+  simp [getElem?_ge, h]
 
-@[deprecated getD_getElem? (since := "2024-12-11")] abbrev getD_get? := @getD_getElem?
+theorem getD_get? (a : Array α) (i : Nat) (d : α) :
+  Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
+  if h : i < a.size then
+    simp [setIfInBounds, h, getElem?_def]
+  else
+    have p : i ≥ a.size := Nat.le_of_not_gt h
+    simp [setIfInBounds, getElem?_len_le _ p, h]
 
 @[simp] theorem getD_eq_get? (a : Array α) (n d) : a.getD n d = (a[n]?).getD d := by
-  simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_getElem?, *]
+  simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_get?, *]
 
 theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
 
 @[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) :
     a.get! i = (a.get? i).getD default := by
   by_cases p : i < a.size <;>
-  simp only [get!_eq_getD, getD_eq_get?, getD_getElem?, p, get?_eq_getElem?]
+  simp only [get!_eq_getD, getD_eq_get?, getD_get?, p, get?_eq_getElem?]
+
+/-! # set -/
+
+@[simp] theorem getElem_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
+      (eq : i = j) (p : j < (a.set i v).size) :
+    (a.set i v)[j]'p = v := by
+  cases a
+  simp
+  simp [set, ← getElem_toList, ←eq]
+
+@[simp] theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
+    (pj : j < (a.set i v).size) (h : i ≠ j) :
+    (a.set i v)[j]'pj = a[j]'(size_set a i v _ ▸ pj) := by
+  simp only [set, ← getElem_toList, List.getElem_set_ne h]
+
+theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
+    (h : j < (a.set i v).size) :
+    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ ▸ h) := by
+  by_cases p : i = j <;> simp [p]
+
+@[simp] theorem getElem?_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
+    (a.set i v)[i]? = v := by simp [getElem?_lt, h]
+
+@[simp] theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
+    (ne : i ≠ j) : (a.set i v)[j]? = a[j]? := by
+  by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
+
+/-! # setIfInBounds -/
+
+@[simp] theorem set!_is_setIfInBounds : @set! = @setIfInBounds := rfl
+
+@[simp] theorem size_setIfInBounds (a : Array α) (index : Nat) (val : α) :
+    (Array.setIfInBounds a index val).size = a.size := by
+  if h : index < a.size  then
+    simp [setIfInBounds, h]
+  else
+    simp [setIfInBounds, h]
+
+theorem getElem_setIfInBounds (a : Array α) (i : Nat) (v : α) (j : Nat)
+    (hj : j < (setIfInBounds a i v).size) :
+  (setIfInBounds a i v)[j]'hj = if i = j then v else a[j]'(by simpa using hj) := by
+  simp only [setIfInBounds]
+  split
+  · simp [getElem_set]
+  · simp only [size_setIfInBounds] at hj
+    rw [if_neg]
+    omega
+
+@[simp] theorem getElem_setIfInBounds_eq (a : Array α) {i : Nat} (v : α) (h : _) :
+    (setIfInBounds a i v)[i]'h = v := by
+  simp at h
+  simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_eq]
+
+@[simp] theorem getElem_setIfInBounds_ne (a : Array α) {i : Nat} (v : α) {j : Nat}
+    (hj : j < (setIfInBounds a i v).size) (h : i ≠ j) :
+    (setIfInBounds a i v)[j]'hj = a[j]'(by simpa using hj) := by
+  simp [getElem_setIfInBounds, h]
+
+@[simp]
+theorem getElem?_setIfInBounds_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) :
+    (a.setIfInBounds i v)[i]? = some v := by
+  simp [getElem?_lt, p]
+
+/-- Simplifies a normal form from `get!` -/
+@[simp] theorem getD_get?_setIfInBounds (a : Array α) (i : Nat) (v d : α) :
+    Option.getD (setIfInBounds a i v)[i]? d = if i < a.size then v else d := by
+  by_cases h : i < a.size <;>
+    simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_get?]
 
 /-! # ofFn -/
 
@@ -1185,6 +1092,9 @@ theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a
     (h : i ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
   simp only [set, ← getElem_toList, List.getElem_set_ne h]
 
+theorem set_set (a : Array α) (i : Nat) (h) (v v' : α) :
+    (a.set i v h).set i v' (by simp [h]) = a.set i v' := by simp [set, List.set_set]
+
 private theorem fin_cast_val (e : n = n') (i : Fin n) : e ▸ i = ⟨i.1, e ▸ i.2⟩ := by cases e; rfl
 
 theorem swap_def (a : Array α) (i j : Nat) (hi hj) :
@@ -2088,6 +1998,14 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   apply ext'
   simp
 
+@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
+    l.toArray.setIfInBounds i a  = (l.set i a).toArray := by
+  apply ext'
+  simp only [setIfInBounds]
+  split
+  · simp
+  · simp_all [List.set_eq_of_length_le]
+
 @[simp] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}:
     l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray := by
   apply ext'
@@ -2406,8 +2324,8 @@ abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero
 
 @[deprecated set!_is_setIfInBounds (since := "2024-11-24")] abbrev set_is_setIfInBounds := @set!_is_setIfInBounds
 @[deprecated size_setIfInBounds (since := "2024-11-24")] abbrev size_setD := @size_setIfInBounds
-@[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_self
-@[deprecated getElem?_setIfInBounds_eq (since := "2024-11-24")] abbrev get?_setD_eq := @getElem?_setIfInBounds_self
+@[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_eq
+@[deprecated getElem?_setIfInBounds_eq (since := "2024-11-24")] abbrev get?_setD_eq := @getElem?_setIfInBounds_eq
 @[deprecated getD_get?_setIfInBounds (since := "2024-11-24")] abbrev getD_setD := @getD_get?_setIfInBounds
 @[deprecated getElem_setIfInBounds (since := "2024-11-24")] abbrev getElem_setD := @getElem_setIfInBounds
 

src/Init/Data/Float32.lean

@@ -9,9 +9,6 @@ import Init.Data.Int.Basic
 import Init.Data.ToString.Basic
 import Init.Data.Float
 
-/-
-#exit -- TODO: Remove after update stage0
-
 -- Just show FloatSpec is inhabited.
 opaque float32Spec : FloatSpec := {
   float := Unit,
@@ -130,7 +127,7 @@ Returns an undefined value if `x` is not finite.
 instance : ToString Float32 where
   toString := Float32.toString
 
-@[extern "lean_uint64_to_float"] opaque UInt64.toFloat32 (n : UInt64) : Float32
+@[extern "lean_uint64_to_float32"] opaque UInt64.toFloat32 (n : UInt64) : Float32
 
 instance : Inhabited Float32 where
   default := UInt64.toFloat32 0
@@ -177,4 +174,6 @@ Efficiently computes `x * 2^i`.
 -/
 @[extern "lean_float32_scaleb"]
 opaque Float32.scaleB (x : Float32) (i : @& Int) : Float32
--/
+
+@[extern "lean_float32_to_float"] opaque Float32.toFloat : Float32 → Float
+@[extern "lean_float_to_float32"] opaque Float.toFloat32 : Float → Float32

src/Init/Data/List/Lemmas.lean

@@ -253,14 +253,6 @@ theorem getElem_eq_getElem?_get (l : List α) (i : Nat) (h : i < l.length) :
     l[i] = l[i]?.get (by simp [getElem?_eq_getElem, h]) := by
   simp [getElem_eq_iff]
 
-theorem getD_getElem? (l : List α) (i : Nat) (d : α) :
-    l[i]?.getD d = if p : i < l.length then l[i]'p else d := by
-  if h : i < l.length then
-    simp [h, getElem?_def]
-  else
-    have p : i ≥ l.length := Nat.le_of_not_gt h
-    simp [getElem?_eq_none p, h]
-
 @[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl
 
 theorem getElem_cons {l : List α} (w : i < (a :: l).length) :

src/Init/Data/List/ToArray.lean

@@ -363,12 +363,4 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
     l.toArray.takeWhile p = (l.takeWhile p).toArray := by
   simp [Array.takeWhile, takeWhile_go_toArray]
 
-@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
-    l.toArray.setIfInBounds i a  = (l.set i a).toArray := by
-  apply ext'
-  simp only [setIfInBounds]
-  split
-  · simp
-  · simp_all [List.set_eq_of_length_le]
-
 end List

src/Init/Data/OfScientific.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Meta
 import Init.Data.Float
+import Init.Data.Float32
 import Init.Data.Nat.Log2
 
 /-- For decimal and scientific numbers (e.g., `1.23`, `3.12e10`).
@@ -56,3 +57,34 @@ instance : OfNat Float n   := ⟨Float.ofNat n⟩
 
 abbrev Nat.toFloat (n : Nat) : Float :=
   Float.ofNat n
+
+/-- Computes `m * 2^e`. -/
+def Float32.ofBinaryScientific (m : Nat) (e : Int) : Float32 :=
+  let s := m.log2 - 63
+  let m := (m >>> s).toUInt64
+  let e := e + s
+  m.toFloat32.scaleB e
+
+protected opaque Float32.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float32 :=
+  if s then
+    let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division
+    let m := (m <<< (3 * e + s)) / 5^e
+    Float32.ofBinaryScientific m (-4 * e - s)
+  else
+    Float32.ofBinaryScientific (m * 5^e) e
+
+instance : OfScientific Float32 where
+  ofScientific := Float32.ofScientific
+
+@[export lean_float32_of_nat]
+def Float32.ofNat (n : Nat) : Float32 :=
+  OfScientific.ofScientific n false 0
+
+def Float32.ofInt : Int → Float
+  | Int.ofNat n => Float.ofNat n
+  | Int.negSucc n => Float.neg (Float.ofNat (Nat.succ n))
+
+instance : OfNat Float32 n   := ⟨Float32.ofNat n⟩
+
+abbrev Nat.toFloat32 (n : Nat) : Float32 :=
+  Float32.ofNat n

src/library/compiler/ir_interpreter.cpp

@@ -187,11 +187,7 @@ option_ref<decl> find_ir_decl(environment const & env, name const & n) {
 }
 
 extern "C" double lean_float_of_nat(lean_obj_arg a);
-
-// TODO: define in Lean like `lean_float_of_nat`
-float lean_float32_of_nat(lean_obj_arg a) {
-    return lean_float_of_nat(a);
-}
+extern "C" float lean_float32_of_nat(lean_obj_arg a);
 
 static string_ref * g_mangle_prefix = nullptr;
 static string_ref * g_boxed_suffix = nullptr;
@@ -257,7 +253,7 @@ union value {
 object * box_t(value v, type t) {
     switch (t) {
     case type::Float:   return box_float(v.m_float);
-    case type::Float32: return box_float(v.m_float32);
+    case type::Float32: return box_float32(v.m_float32);
     case type::UInt8:   return box(v.m_num);
     case type::UInt16:  return box(v.m_num);
     case type::UInt32:  return box_uint32(v.m_num);

src/runtime/object.h

@@ -373,6 +373,7 @@ inline unsigned unbox_uint32(b_obj_arg o) { return lean_unbox_uint32(o); }
 inline obj_res box_uint64(unsigned long long v) { return lean_box_uint64(v); }
 inline unsigned long long unbox_uint64(b_obj_arg o) { return lean_unbox_uint64(o); }
 inline obj_res box_float(double v) { return lean_box_float(v); }
+inline obj_res box_float32(float v) { return lean_box_float32(v); }
 inline double unbox_float(b_obj_arg o) { return lean_unbox_float(o); }
 inline float unbox_float32(b_obj_arg o) { return lean_unbox_float32(o); }
 inline obj_res box_size_t(size_t v) { return lean_box_usize(v); }

tests/lean/run/float32.lean

@@ -0,0 +1,38 @@
+/-- info: 2.100000 -/
+#guard_msgs in
+#eval (2.1 : Float32)
+
+/-- info: 3.200000 -/
+#guard_msgs in
+#eval (2.1 : Float32) + 1.1
+
+/-- info: 0.900000 -/
+#guard_msgs in
+#eval (2.1 : Float32) - 1.2
+
+def test1 : IO Unit := do
+  IO.println ((2 : Float32).sin);
+  IO.println ((2 : Float32).cos);
+  IO.println ((2 : Float32).sqrt);
+  IO.println ((2 : Float32) ^ (100 : Float32));
+
+/--
+info: 0.909297
+-0.416147
+1.414214
+1267650600228229401496703205376.000000
+-/
+#guard_msgs in
+#eval test1
+
+/-- info: 0.909297 -/
+#guard_msgs in
+#eval (2 : Float32).sin.toFloat
+
+/-- info: 0.909297 -/
+#guard_msgs in
+#eval (2 : Float).sin.toFloat32
+
+/-- info: 1606938044258990275541962092341162602522202993782792835301376.000000 -/
+#guard_msgs in
+#eval (2 : Float32).toFloat ^ (200 : Float32).toFloat