## Stream: new members

### Topic: identity type and refl

#### Shaun Steenkamp (Nov 13 2018 at 15:46):

Is it possible to pattern match on the refl constructor of the identity type (eq.refl) in Lean similar to what one can do in Agda? I tried defining one by pattern matching but it didn't seem to work.

#### Mario Carneiro (Nov 13 2018 at 15:50):

yes, there are several ways

#### Mario Carneiro (Nov 13 2018 at 15:51):

subst and cases both work, as does the pattern matcher

#### Mario Carneiro (Nov 13 2018 at 15:52):

note that one side of the equality must be a variable and must participate in the pattern match (be right of the colon) for it to work

#### Reid Barton (Nov 13 2018 at 15:52):

Can you give an example of code you expect to work but doesn't?

#### Shaun Steenkamp (Nov 13 2018 at 15:53):

def subst {A : Type ℓ}(P : A → Type ℓ'){a b : A} : a = b → P a → P b :=
assume p : a = b,
assume x : P a,
show P b, from eq.cases_on p x


works fine

but then

#### Shaun Steenkamp (Nov 13 2018 at 15:54):

def subst_const
{A : Type ℓ}
{B : Type ℓ'}
{x y : A}
: Π
(p : x = y)
(b : B)
, ---------------------
subst (λ _ , B) p b = b
| (eq.refl) _ := eq.refl


doesn't work

#### Shaun Steenkamp (Nov 13 2018 at 15:55):

This is something I've used a lot in Agda, and I figured if I try to do some of these "basic" things in Lean that could help me learn it, but I think that maybe I don't understand the basic syntax well enough yet...

#### Reid Barton (Nov 13 2018 at 15:55):

Yes, that is because the requirement "one side of the equality must be a variable and must participate in the pattern match (be right of the colon)" (or in this case, below the colon :slight_smile:) is not met

#### Reid Barton (Nov 13 2018 at 15:58):

y needs to move past the colon, and the last line should read | _ (eq.refl _) _ := eq.refl _

#### Reid Barton (Nov 13 2018 at 15:59):

or replace eq.refl _ with rfl

#### Shaun Steenkamp (Nov 13 2018 at 15:59):

okay, got it, can I still keep y implicit?

it seems I can

#### Shaun Steenkamp (Nov 13 2018 at 16:01):

thank you very much for your help!! ^_^

Last updated: May 16 2021 at 20:13 UTC