How to use agda2-make-case

gistfile1.hs

module Agdacase where

data Nat : Set where
  zero : Nat
  succ : (n : Nat) -> Nat
-- an example : n += 2
succsucc : Nat -> Nat
succsucc n = {! !} -- try to type C-c C-c `in the goal'
-- then you should type the variable `n' in the minibuffer

-- finally you must get the following instead!
-- succsucc : Nat -> Nat
-- succsucc zero = {!!}
-- succsucc (succ n) = {!!}