Definition df-lpad

Description: Define the leftpad function. (Contributed by Thierry Arnoux, 7-Aug-2023)

	Ref	Expression
Assertion	df-lpad	|- leftpad = ( c e. _V , w e. _V |-> ( l e. NN0 |-> ( ( ( 0 ..^ ( l - ( # ` w ) ) ) X. { c } ) ++ w ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clpad	|- leftpad
1		vc	|- c
2		cvv	|- _V
3		vw	|- w
4		vl	|- l
5		cn0	|- NN0
6		cc0	|- 0
7		cfzo	|- ..^
8	4	cv	|- l
9		cmin	|- -
10		chash	|- #
11	3	cv	|- w
12	11 10	cfv	|- ( # ` w )
13	8 12 9	co	|- ( l - ( # ` w ) )
14	6 13 7	co	|- ( 0 ..^ ( l - ( # ` w ) ) )
15	1	cv	|- c
16	15	csn	|- { c }
17	14 16	cxp	|- ( ( 0 ..^ ( l - ( # ` w ) ) ) X. { c } )
18		cconcat	|- ++
19	17 11 18	co	|- ( ( ( 0 ..^ ( l - ( # ` w ) ) ) X. { c } ) ++ w )
20	4 5 19	cmpt	|- ( l e. NN0 |-> ( ( ( 0 ..^ ( l - ( # ` w ) ) ) X. { c } ) ++ w ) )
21	1 3 2 2 20	cmpo	|- ( c e. _V , w e. _V |-> ( l e. NN0 |-> ( ( ( 0 ..^ ( l - ( # ` w ) ) ) X. { c } ) ++ w ) ) )
22	0 21	wceq	|- leftpad = ( c e. _V , w e. _V |-> ( l e. NN0 |-> ( ( ( 0 ..^ ( l - ( # ` w ) ) ) X. { c } ) ++ w ) ) )