Are reflection tests run?

[JacquesCarette]

For example, is this file actually used?

It appears that these lines https://github.com/agda/agda-stdlib/blob/94906c00c9b0afab2283149fa33875e31b226a61/tests/reflection/assumption/Main.agda#L54-L58 are wrong and instead should be printed "in context" which concatMap doesn't do.

The original report (on the Univalent Agda Discord) was that this code

printTelescope : Telescope → TC ⊤
printTelescope [] = returnTC tt
printTelescope ((id , (arg info t)) ∷ ts) =
 do printTelescope ts
    debugPrint "" 1 (strErr id ∷ strErr " : " ∷ termErr t ∷ [])

didn't do the right thing, and should instead have the second case be

printTelescope ((id , (arg info t)) ∷ ts) =
 do printTelescope ts
    inContext ts do
      debugPrint "" 1 (strErr id ∷ strErr " : " ∷ termErr t ∷ [])

The relation is that (apparently) the author of printTelescope was copying out (and expanding) the code in that example.

I have never used any of the reflection stuff myself, so I'm just reporting. @gallais seems to be the author.

[gallais]

They are run, however without any logging so this debugging code is not printed.