Changes related to a change to Agda's reflection machinery.

[nad]

The reflection machinery now supports erasure (in Arg), see agda/agda#5317.

I made the code compile, but further changes may be warranted:

• I did not write anything in the changelog.

• I did not add any deprecation warnings.

• I changed the semantics of Tactic.RingSolver.Core.ReflectionHelp.getVisible.

• The function showTerm does not print erasure annotations (but it also does not print relevance annotations).

[MatthewDaggitt]

Thanks!

I did not write anything in the changelog.

I think the changes do need to be documented, a brief description of the new changes/modules + a pointer to the Agda 2.6.2 CHANGELOG?

I did not add any deprecation warnings.

I think that's fine. The reflection API is undergoing a lot of churn at the moment, I don't think it's feasible to hide it from the user.

I changed the semantics of Tactic.RingSolver.Core.ReflectionHelp.getVisible.

That doesn't need to be documented as it's in a Core module which we do not guarantee the backwards compatibility for.

The function showTerm does not print erasure annotations (but it also does not print relevance annotations).

That would be good to fix while we're here! It should be pretty easy right?

[nad]

I think the changes do need to be documented, a brief description of the new changes/modules + a pointer to the Agda 2.6.2 CHANGELOG?

My idea was to leave this to you, so that you get things the way you want them. However, I've written something now.

The function showTerm does not print erasure annotations (but it also does not print relevance annotations).

That would be good to fix while we're here! It should be pretty easy right?

I don't want to spend time adding features to the standard library right now. I think I've addressed your other remarks.

[MatthewDaggitt]

Opened #1491 for the printing of argument annotations.