Correct, Agda has this notion of reflection. The way to do "tactics" in Agda is simply to manipulate expressions, and there's no meta-language in which to do th

Correct, Agda has this notion of reflection. The way to do "tactics" in Agda is simply to manipulate expressions, and there's no meta-language in which to do this: it's just Agda all the way down. It's neat, but not easy.