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 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
@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)
:technologist_g1:
@g I've found that a bit difficult in idris too...
@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)