Documentation

Batteries.Lean.Delaborator

@[deprecated Lean.MessageData.ofConst]

Abbreviation for Lean.MessageData.ofConst.

Equations
Instances For