 One of the approaches to termination checking in dependently typed programming languages are sized types.The main idea is to annotate the types over which we can recurse with size annotations and allow recursive calls only on smaller arguments.Sized types are implemented in Agda as a syntactic extension.