Auxillary definitions related to Lean.RArray
that are typically only used in meta-code, in
particular the ToExpr
instance.
Instances For
Instances For
Equations
Instances For
Equations
- Lean.instToExprRArray = { toExpr := fun (a : Lean.RArray α) => Lean.RArray.toExpr (Lean.toTypeExpr α) Lean.toExpr a, toTypeExpr := Lean.mkApp (Lean.mkConst `Lean.RArray) (Lean.toTypeExpr α) }