Metamath Proof Explorer


Syntax definition clpad

Description: Extend class notation with the leftpad function.

Ref Expression
Assertion clpad class leftpad