This is currently hacked up in several places, e.g., via mapping into nums then using sptrees.

In particular, it would be great to reuse some of the infrastructure (if any) from HOL-Theorem-Prover/HOL#1780

The CakeML implementation could come in several flavors to support the relevant use cases (e.g., both pure and stateful).