Metamath Proof Explorer

Syntax definition clpad

Description: Extend class notation with the leftpad function.

Ref Expression
Assertion clpad class leftpad