Pattern-matchingLambdas

See the official user manual for the most up-to-date version of the information on this page.

    \ { pattern  -> exp
      ; pattern1 -> exp1
      ...
      }

Also if you are using agda-stdlib you can import 'Function' to get the case_of_ and be able to write

    case exp of
    \ { pattern -> exp1
      ; ...
      }