FunPropM

Mathlib.Tactic.FunProp.Types

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.FunProp.FunPropM

Lean4

/-- Monad to run `fun_prop` tactic in. -/
abbrev FunPropM :=
  ReaderT FunProp.Context <| StateT FunProp.State MetaM

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

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

Разделы

Аффилиация

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