Not sure what GP is thinking of, but here's an example of embedding tools for reasoning about performance in Idris: https://www.youtube.com/watch?v=4i7KrG1Afbk&feature=youtu.be...