parameter-number := λ(: tt Type)(: parameter-name String). (: ( (let a 0_u64) (match tt ( () ( (TGround( _ ps )) ( (set a (parameter-number( ps parameter-name 1_u64 ))) )) ( _ () ) )) a ) U64); parameter-number := λ(: tt List)(: parameter-name String)(: pi U64). (: ( (let a 0_u64) (match tt ( () ( (LCons( (TVar v) rst )) ( (if (==( v parameter-name )) ( (set a pi) ) ( (set a (parameter-number( rst parameter-name (+( pi 1_u64 )) ))) )) )) ( _ () ) )) a ) U64);