[Agda] Termination checker and rewriting

[Guillaume GENESTIER]

Dear all,

I am looking for information about the checks performed when rewriting 
rules are declared in Agda.

More specifically, I was wondering if any termination checking is 
performed on these rules.

The only information I was able to find in the Agda manual is that the 
rewriting machinery is "experimental and totally unsafe". On the other 
hand, termination (and totality) checking is performed when a function 
is declared inductively.

Faithfully yours,

Guillaume Genestier,

ENS Paris-Saclay and MINES ParisTech