Zulip Chat Archive

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

Kenny Lau (May 19 2020 at 14:12):

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: Dec 20 2023 at 11:08 UTC