# Zulip Chat Archive

## Stream: new members

### Topic: constraints on pattern matching

#### Shi Zhengyu (Jan 05 2022 at 08:09):

Hi all,

Is there a way to apply additional propositional constraints on pattern matching? e.g.

```
def Id (n: ℕ): finMat n n
| ⟨x, _⟩ ⟨x2, _⟩ := if (x == x2) then 1 else 0
```

How should I replace the `if ... then .. else`

part with actual Lean code?

Thanks!

#### Kevin Buzzard (Jan 05 2022 at 08:15):

I think Lean has `if...then...else`

?

#### Yaël Dillies (Jan 05 2022 at 08:16):

Maybe you'll consider docs#ite or docs#dite actual Lean code?

#### Shi Zhengyu (Jan 05 2022 at 08:18):

Kevin Buzzard said:

I think Lean has

`if...then...else`

?

Lol thanks :joy: that was unexpected

#### Shi Zhengyu (Jan 05 2022 at 08:22):

By the way, the below definition fail with `polyId is noncomputable`

, may I ask what exactly does `noncomputable`

mean? I vaguely think it's connected with axiom of choice ...

```
import data.fin.basic
import data.complex.basic
import data.matrix.basic
import data.matrix.notation
import data.polynomial.basic
def finPolyMat (u: ℕ) (v: ℕ) := matrix (fin u) (fin v) (polynomial ℂ)
def polyId (n: ℕ): finPolyMat n n := λ u v: fin n, if u = v then 1 else 0
```
```

#### Yaël Dillies (Jan 05 2022 at 08:27):

It means Lean can't generate bytecode (aka computation instructions) for it. So you can't run the code but you can still prove stuff about it.

#### Yaël Dillies (Jan 05 2022 at 08:28):

Given that Lean can generate bytecode for all axioms except the axiom of choice (and `sorry`

but you won't use it in final code), noncomputability is indeed linked to using the axiom of choice.

Last updated: Dec 20 2023 at 11:08 UTC