ok so. consider this contrived thing:

Inductive tree := Tree (xs: list tree).
Fixpoint nodes t :=
match t with Tree xs =>
fold_left plus (map nodes xs) 0
end.

coq accepts this as terminating. (idris and agda both reject it). so... why? does it just expand all definitions before checking, or what? the manual doesn't seem to mention this behaviour

(if you do `Compute nodes.` you get something pretty hairy but now acceptable according to the rules in the manual)

@g does coq assume inductive types are finite?

@lizardsquid you mean that the values of the type are finite, or that there's only a finite amount of possible values?

(it makes sure that inductive values are always finite with a couple of restrictions on datatypes & recursive functions, if you meant the first one)

@g the first - because I *think* (not certain) that the nodes function can be shown to be monotonically decreasing the size of the data structure, and coq might by deriving that proof automatically