## Stream: new members

### Topic: pattern

#### Kenny Lau (May 19 2020 at 14:02):

universe u

inductive free_magma (α : Type u) : Type u
| of : α → free_magma
| mul : free_magma → free_magma → free_magma

instance {α : Type u} : has_mul (free_magma α) :=
⟨free_magma.mul⟩

attribute [pattern] free_magma.mul

def test {α : Type u} : free_magma α → unit
| (free_magma.of x) := ()
| (x * y) := () -- invalid pattern, must be an application, constant, variable, type ascription, aliasing pattern or inaccessible term

def test' : ℕ → unit
| 0 := ()
| (n + 1) := ()


#### Kenny Lau (May 19 2020 at 14:02):

how do I make lean recognize x * y as a pattern?

#### Kevin Buzzard (May 19 2020 at 14:03):

I never really understood why (n + 1) works with nat.

#### Reid Barton (May 19 2020 at 14:04):

I thought the way you are doing it was supposed to work.

#### Kevin Buzzard (May 19 2020 at 14:06):

I think add is marked as the pattern for nat, but it's succ which is being picked up. Have I misremembered? I could never see the logic.

#### Reid Barton (May 19 2020 at 14:08):

Oh hmm, now I'm not sure.

#### Reid Barton (May 19 2020 at 14:09):

The algorithm must be something like: if Lean wants a pattern but it sees an application of something that is not a constructor, unfold the definition of that thing. Then pattern must control this unfolding somehow but I don't know exactly how that works.

#### Alex J. Best (May 19 2020 at 14:10):

attribute [pattern] has_mul.mul


works

#### Kenny Lau (May 19 2020 at 14:10):

but wouldn't this make every other multiplication a pattern?

#### Kenny Lau (May 19 2020 at 14:11):

is this a good attribute?

#### Kevin Buzzard (May 19 2020 at 14:12):

I'm not at lean right now. Is has_add.add a pattern? You can check with #print

yes it is

#### Kevin Buzzard (May 19 2020 at 14:13):

Well this attribute is clearly not causing too much harm

#### Kevin Buzzard (May 19 2020 at 14:14):

Why not make a new branch of mathlib, add the attribute to * in logic.basic, push and see if CI compiles mathlib

#### Kenny Lau (May 19 2020 at 14:15):

https://github.com/leanprover-community/lean/blob/master/library/init/core.lean#L400

#### Kenny Lau (May 19 2020 at 14:15):

attribute [pattern] has_zero.zero has_one.one bit0 bit1 has_add.add has_neg.neg


#### Reid Barton (May 19 2020 at 14:17):

I would guess nothing should change, since it should be impossible to use * in a pattern currently and therefore there must not be any such usages.

Last updated: May 13 2021 at 17:42 UTC