niss@chitter.xyz 
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)
:technologist_g1:
@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)
:technologist_g1:
@g I've found that a bit difficult in idris too...
@lizardsquid no you're right it does decrease, it's just that idris isn't as good at seeing that as coq which is a bit of a shame (and it might be unavoidable, but im not sure)