[Agda] Programming with well-founded/sized recursion

[Xuanrui Qi]

Hello,

One of my current Agda developments involve some kind of well-
founded/measure-based recursion. The original development was in Coq,
where I used measure-based termination. Now, as I transcribe my code to
Agda, what should I use to prove termination to the termination checker
?

The data structure I am operating on is a tree, and the termination
proof is just by induction on size. Sized types seem like a good choice
for what I want, but it's hard to find resources to get me started. Are
there any pointers or examples (besides the manual)? Alternatively, are
there combinators that can help me define this kind of recursion using
accessibility predicates?

Which would be the preferred solution if I want to compile my code
eventually?

Thanks,
Xuanrui