CastMode

Mathlib.Tactic.DepRewrite

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.DepRewrite.CastMode

Lean4

/-- See `Config.castMode`. -/
inductive CastMode where/-- Only insert casts on proofs.

  In this mode, it is *not* permitted to cast subterms of proofs that are not themselves proofs. -/
-- TODO: should we relax this restriction and switch `castMode` when visiting a proof?


  | proofs/-- Insert casts whenever necessary. -/

  | all
  deriving BEq

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru