summaryrefslogtreecommitdiff
path: root/src/Obs/Typing.idr
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2022-12-18 13:38:54 +0000
committerGreg Brown <greg.brown01@ed.ac.uk>2022-12-18 13:38:54 +0000
commit00bab44d15ca4e1f0d77cfc8351056d22b83e225 (patch)
treec98e9cb3c197e94c7d8db6aea50dc24d8bdd9694 /src/Obs/Typing.idr
parent88b6df5dd91c062a96e646e6e6b0ac5fd57b7c03 (diff)
Make the parser commit to the choices it makes.
Diffstat (limited to 'src/Obs/Typing.idr')
0 files changed, 0 insertions, 0 deletions