Tagging of unfold boundaries for translation attributes

The file Mathlib.Tactic.Translate.UnfoldBoundary defines how to add unfold boundaries in terms. In this file, we define the infrastructure for tagging declaration to be used for that. This is in a separate file, because we need to import Mathlib.Tactic.Translate.Core here.

def Mathlib.Tactic.Translate.elabInsertCast (declName : Lean.Ident) (valStx : Lean.Term) (t : TranslateData) : Lean.Elab.Command.CommandElabM Unit

The insert_cast foo := ... command should be used when the translation of some definition foo is not definitionally equal to the translation of its value. It requires a proof that these two are equal. For example,

to_dual_insert_cast Monotone := by grind

If the definition is a type, you should use insert_cast_fun instead.

The command internally generates an unfolding theorem for foo, and a translation of this theorem. When type checking a term requires the definition foo to be unfolded, then in order to translate that term, a cast is first inserted into the term using this unfolding theorem. As a result, type checking the term won't anymore require unfolding foo, so the term can be safely translated.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Translate.elabInsertCastFun (declName : Lean.Ident) (valStx₁ valStx₂ : Lean.Term) (t : TranslateData) : Lean.Elab.Command.CommandElabM Unit

The insert_cast_fun foo := ..., ... command should be used when the translation of some type foo is not definitionally equal to the translation of its value. It requires a function from the translation of foo to the translation of the value of foo, and a function in the opposite direction. For example,

to_dual_insert_cast_fun DecidableLE := fun inst a b ↦ inst b a, fun inst a b ↦ inst b a

The command internally generates these unfold/refold functions for foo, and their translations. If type checking a term requires the definition foo to be unfolded, then before translating that term, the unfold/refold function is inserted into the term. As a result, type checking the term won't anymore require unfolding foo, so the term can be safely translated. After translating, the unfold/refold functions are again unfolded.

Equations

• One or more equations did not get rendered due to their size.