The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

Hi,

> Finite maps are based on finite functions which allow such nested
definitions,
> You can find an example in the doc:

There is actually an example about tree in the header

https://github.com/math-comp/math-comp/blob/17dd3091e7f809c1385b0c0be43d1f8de4fa6be0/mathcomp/ssreflect/finfun.v#L24

the depth function is simply:

 Inductive tree : Type := node n of tree ^ n.
 Fixpoint depth (t : tree) : nat :=
  match t with node n br => (\max_(i <- codom (depth \o br)) i).+1
  end.

--
Laurent