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

Actually I think it's fine. Only the first line is meant to be represented anyway.