Zulip Chat Archive

Stream: new members

Topic: pattern


view this post on Zulip 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) := ()

view this post on Zulip Kenny Lau (May 19 2020 at 14:02):

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

view this post on Zulip Kevin Buzzard (May 19 2020 at 14:03):

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

view this post on Zulip Reid Barton (May 19 2020 at 14:04):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 19 2020 at 14:08):

Oh hmm, now I'm not sure.

view this post on Zulip 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.

view this post on Zulip Alex J. Best (May 19 2020 at 14:10):

attribute [pattern] has_mul.mul

works

view this post on Zulip Kenny Lau (May 19 2020 at 14:10):

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

view this post on Zulip Kenny Lau (May 19 2020 at 14:11):

is this a good attribute?

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 19 2020 at 14:12):

yes it is

view this post on Zulip Kevin Buzzard (May 19 2020 at 14:13):

Well this attribute is clearly not causing too much harm

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 19 2020 at 14:15):

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

view this post on Zulip Kenny Lau (May 19 2020 at 14:15):

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

view this post on Zulip 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