 Primitive recursive syntax and arity checking

For a decidable coding of finite construction trees, the codes of arity-$i$ primitive recursive functions in intension are decidable. Check initial-function tags, then verify the child arities at each composition and recursion node. This is a terminating finite syntax check, distinct from asking whether an arbitrary program's extension happens to be primitive recursive.