Closed fredrik-bakke closed 1 year ago
If you have autoclosing brackets enabled, and try to type any character in agda-input that requires a ( or a {, for instance ⦃, then agda-input will be interrupted, and you will get () or {} in your code instead.
(
{
⦃
()
{}
If you have autoclosing brackets enabled, and try to type any character in agda-input that requires a
(
or a{
, for instance⦃
, then agda-input will be interrupted, and you will get()
or{}
in your code instead.