updateConstantVal — Mathlib

Lean4
/-- Update `ConstantVal` (the data common to all constructors of `ConstantInfo`)
in a `ConstantInfo`. -/
def updateConstantVal : ConstantInfo → ConstantVal → ConstantInfo
  | defnInfo info, v => defnInfo { info with toConstantVal := v }
  | axiomInfo info, v => axiomInfo { info with toConstantVal := v }
  | thmInfo info, v => thmInfo { info with toConstantVal := v }
  | opaqueInfo info, v => opaqueInfo { info with toConstantVal := v }
  | quotInfo info, v => quotInfo { info with toConstantVal := v }
  | inductInfo info, v => inductInfo { info with toConstantVal := v }
  | ctorInfo info, v => ctorInfo { info with toConstantVal := v }
  | recInfo info, v => recInfo { info with toConstantVal := v }
Похожие утверждения