[Agda] debugPrint : Does it work correctly?

Apostolis Xekoukoulotakis apostolis.xekoukoulotakis at gmail.com
Tue Mar 6 20:36:44 CET 2018


I do know how verbosity levels work.

According to
https://github.com/agda/agda/blob/9ff3310f27a006675656d453d3338df233e4ca78/CHANGELOG.md#reflection

the String at debugPrint seems to act like a filter.

I have tested it with multiple values and it does not seem to filter the
logs at the *Agda debug* buffer.

Am I misinterpreting something?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180306/eeb7fa37/attachment.html>


More information about the Agda mailing list