Restore agda-input for ordinary backslash (regression in #6769)

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.

https://wiki.portal.chalmers.se/agda/pmwiki.php

Other

2.48k stars 345 forks source link

Restore agda-input for ordinary backslash (regression in #6769) #7213

Closed andreasabel closed 6 months ago

andreasabel commented 6 months ago

We need to be able to type ordinary backslashes e.g. in regular expressions.

ATTN: @gallais @UlfNorell @fredrik-bakke

fredrik-bakke commented 6 months ago

Terribly sorry for the mistake!

andreasabel commented 6 months ago

Terribly sorry for the mistake!

No problem.

Additions to the agda input mode are always welcome!
They should be backward compatible, though, as folks have gotten used to the existing key bindings.