summaryrefslogtreecommitdiff
path: root/src/Inky/Term.idr
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2024-11-12 18:13:22 +0000
committerGreg Brown <greg.brown01@ed.ac.uk>2024-11-12 18:13:22 +0000
commit865dc549baf613e45e2f79036d54850a483fa509 (patch)
tree1638d8bf6544ede436a3d933dcdc2c0faf59727c /src/Inky/Term.idr
parent6ce6cf4580f2c0ab4c7c4ec56f438c1cc184c7cd (diff)
Fix bad annotation when desugaring map.
Diffstat (limited to 'src/Inky/Term.idr')
0 files changed, 0 insertions, 0 deletions