[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