Zulip Chat Archive

Stream: general

Topic: Trouble with recursive function


Daniel Fabian (Aug 11 2020 at 15:25):

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 (Aug 13 2020 at 02:11):

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 (Aug 13 2020 at 02:19):

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


Last updated: Dec 20 2023 at 11:08 UTC