lean auto monomorphize real numbers

Stream: general

[Frederick Pu]

Does lean auto support monomorphizing real numbers into the real numbers in the smt solver yet?

[Frederick Pu]

seems like the manual translation is done here so no real number support im guessing:

def processTypeExpr (e : Expr) : ReifM LamSort := do
  let tyVarMap ← getTyVarMap
  let e ← Reif.resolveTy e
  if let .some idx := tyVarMap.get? e then
    return .atom idx
  match e with
  | .sort lvl =>
    if ← Meta.isLevelDefEq lvl .zero then
      return .base .prop
    else
      newTypeExpr e
  | .const ``Bool [] => return .base .bool
  | .const ``Nat [] => return .base .nat
  | .const ``Int [] => return .base .int
  | .const ``String [] => return .base .string
  | .const ``Empty [] => return .base .empty
  | .app (.const ``BitVec []) nExpr =>
    if let .some n ← @id (MetaM _) (Meta.evalNat nExpr) then
      return .base (.bv n)
    else
      newTypeExpr e
  | _ => newTypeExpr e

https://github.com/leanprover-community/lean-auto/blob/a12f0ef2ffdf214a52f0b457a2e2ccebd934cac2/Auto/Translation/LamReif.lean#L984

[Frederick Pu]

also is there any mechanism currently that allows for the caching of the translated version of lemma databases?