getDontTranslates — Mathlib

Lean4

/-- Given a list of variable local identifiers that shouldn't be translated,
determine the arguments that shouldn't be translated.

TODO: Currently, this function doesn't deduce any `dont_translate` types from `type`.
In the future we would like that the presence of `MonoidAlgebra k G` will automatically
flag `k` as a type to not be translated.
-/
def getDontTranslates (given : List Ident) (type : Expr) : MetaM (List Nat) := do
  forallTelescope type fun xs _ => do
      given.mapM fun id =>
          withRef id.raw <| do
            let fvarId ← getFVarFromUserName id.getId
            return (xs.idxOf? fvarId).get!

Похожие утверждения