By default, agda2-make-case (C-c C-c) only introduces explicit arguments on a case-split. To get it to introduce implicit arguments, the fastest way I know of is to use agda2-display-implicit-arguments (C-c C-x C-h) and then do the case split which fortunately does then turn off display-implicit-arguments. This ends up being quite a long string C-c C-x C-h C-c C-c so it would be nice if this functionality was supported as a prefix argument: C-u C-c C-c.
By default,
agda2-make-case(C-c C-c) only introduces explicit arguments on a case-split. To get it to introduce implicit arguments, the fastest way I know of is to useagda2-display-implicit-arguments(C-c C-x C-h) and then do the case split which fortunately does then turn off display-implicit-arguments. This ends up being quite a long stringC-c C-x C-h C-c C-cso it would be nice if this functionality was supported as a prefix argument:C-u C-c C-c.