[isabelle] Recursion through Types


There is a trick (due to John Harrison) to encode the dimension N of,
e.g., N-bit words with a type argument.  The word libraries in
Isabelle/HOL and HOL4 are based on this approach.

In this setting, what is the recommended way to define a function that
performs recursion over N, i.e., whose result for an (N+1)-bit word is
naturally expressed in terms of its result for an N-bit word?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.