Documentation

Batteries.Lean.Meta.Expr

source
@[implicit_reducible]
instance Lean.Literal.instOrd_batteries :
Ord Literal
Equations
  • One or more equations did not get rendered due to their size.