Pattern-matching Lambdas

    \ { 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
      ; ...
      }