atomicity

Stream: new members

[Julian Berman]

What are atoms in lean, or what does atomicity mean? A couple of times I've made the mistake when pattern matching of doing:

def f : Nat → String
  | 0 => "foo"
  | n.succ => "bar"

instead of

def f : Nat → String
  | 0 => "foo"
  | n + 1 => "bar"

and lean will complain in the former case that "invalid pattern variable, must be atomic" -- I know there's @[matchPattern] or in lean3 @[pattern] which tells lean which things are OK to use in match patterns -- is there anything else I should know as to why lean likes the second example more than the first?

[Mario Carneiro]

I think that error means that you have named a variable with the nonatomic name n.succ

[Mario Carneiro]

Variable names (almost?) always have no namespaces

[Mario Carneiro]

Basically, it's not actually treating it as a projection

[Bryan Gin-ge Chen]

Right, this works:

def f : Nat → String
  | 0 => "foo"
  | Nat.succ n => "bar"

[Julian Berman]

I see! Interesting, thanks.