Documentation

Converts a lifted IR function type to an Agda type expression.

If the type contains decreasing annotations, a size type variable is bound and used to annotate these occurrences.

Converts a constructor type from lifted IR to Agda.

If the constructor contains decreasing arguments (i.e., recursive arguments), a new sized type variable is bound and used to annotate these types.