Lambda Abstraction¶

Pattern matching lambda¶

Anonymous pattern matching functions can be defined using one of the two following syntaxes:

```\ { p11 .. p1n -> e1 ; … ; pm1 .. pmn -> em }

\ where
p11 .. p1n -> e1
…
pm1 .. pmn -> em
```

(where, as usual, `\` and `->` can be replaced by `λ` and `→`). Note that the `where` keyword introduces an indented block of clauses; if there is only one clause then it may be used inline.

Internally this is translated into a function definition of the following form:

```extlam p11 .. p1n = e1
…
extlam pm1 .. pmn = em
```

where extlam is a fresh name. This means that anonymous pattern matching functions are generative. For instance, `refl` will not be accepted as an inhabitant of the type

```(λ { true → true ; false → false }) ==
(λ { true → true ; false → false })
```

because this is equivalent to `extlam1 ≡ extlam2` for some distinct fresh names `extlam1` and `extlam2`. Currently the `where` and `with` constructions are not allowed in (the top-level clauses of) anonymous pattern matching functions.

Examples:

```and : Bool → Bool → Bool
and = λ { true x → x ; false _ → false }

xor : Bool → Bool → Bool
xor = λ { true  true  → false
; false false → false
; _     _     → true
}

eq : Bool → Bool → Bool
eq = λ where
true  true  → true
false false → true
_ _ → false

fst : {A : Set} {B : A → Set} → Σ A B → A
fst = λ { (a , b) → a }

snd : {A : Set} {B : A → Set} (p : Σ A B) → B (fst p)
snd = λ { (a , b) → b }

swap : {A B : Set} → Σ A (λ _ → B) → Σ B (λ _ → A)
swap = λ where (a , b) → (b , a)
```

Regular pattern-matching lambdas are treated as non-erased function definitions. One can make a pattern-matching lambda erased by writing `@0` or `@erased` after the lambda:

```@0 _ : @0 Set → Set
_ = λ @0 { A → A }

@0 _ : @0 Set → Set
_ = λ @erased where
A → A
```