unexpander_op

Mathlib.Data.Opposite

URI: https://scilib.ai/kg/mathlib#Opposite.unexpander_op

Lean4

/-- Make sure that `Opposite.op a` is pretty-printed as `op a` instead of `{ unop := a }` or
`⟨a⟩`. -/
@[app_unexpander Opposite.op]
protected def unexpander_op : Lean.PrettyPrinter.Unexpander
  | s => pure s

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

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

Разделы

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

Аффилиация

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