## 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