Stream: General

Topic: datatype size

Tobias Nipkow (Jan 29 2026 at 12:11):

I have this datatype:
datatype ('n,'t) tree = Sym "('n,'t) sym" | Rule 'n "('n,'t) tree list" datatype_compat tree
The size function I seem to get is not the one I get. I would have liked this one:
fun size_pt :: "('n,'t)tree ⇒ nat" where "size_pt (Sym _) = 0" | "size_pt (Rule _ ts) = sum_list (map size_pt ts) + 1"
But ideally without the _pt, directly out of the datatype definition.

I tried
datatype (plugins del: size)
But now my own definition of size fails, possibly because the recursive call map size_pt ts needs a size function for the termination proof.

It is not a big issue but maybe there is a trick.

Thanks
Tobias

Dmitriy Traytel (Jan 29 2026 at 14:07):

You could use primrec instead of fun.

Tobias Nipkow (Jan 29 2026 at 14:18):

Of course! Thanks

Last updated: Feb 06 2026 at 20:37 UTC