toothbrush/agda-gp — comment on commit e5fe83916fa8e3a3269f09fc93dbdf5764f9e3f0
File:  line 0
By jpcooper:

Does that solve it?