Trouble with recursive function

Stream: general

[Daniel Fabian]

I have an inductive that has a list of children and I'm having real trouble writing a function against it.

inductive sort
| single
| nested (tl : list sort)

def sort.to_sexpr : sort → string
| (sort.single) := ""
| (sort.nested tl) := string.join $ tl.map sort.to_sexpr

In this (simplified) example, I get the error unexpected occurrence of recursive function. Clearly tl.sizeof < (sort.nested tl).sizeof, so I should be allowed to use sort.to_sexpr, no?

On an vaguely related note, it wouldn't let me formulate my sort using a subtype of lists or using a proof of my property.

inductive sort'
| single
| nested (children : {l : list sort' // l.length > 0})

complains, that inductive type being declared cannot occur as an index of another inductive type, so I had to explicitly carry a head element and a tail.

any idea, why my recursive call is not happy?

[Floris van Doorn]

The equation compiler for nested inductive types is not very good / doesn't work.
I'm afraid that the general advice here is to hand-roll your own definition of nested inductive types using mutual/indexed inductive types.

[Mario Carneiro]

I think for your application, you can just go meta and then the equation compiler and nested inductives will work fine