PR summary f0f1d7c49b

Import changes for modified files

No significant changes to the import graph

Declarations diff

No declarations were harmed in the making of this PR! 🐙

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

./scripts/technical-debt-metrics.sh pr_summary

This might need a zulip thread if this is a new style decision, or a pointer to a core style guide if lean itself has already adopted this.

I'm been bitten one too many times by | none matching everything under a variable called none, so personally prefer to always use the . version.

I don't understand what you mean with | none matching everything under a variable named none. I don't think this is possible in a match statement (although it is possible with let, as in let none := 5).

def foo (n : Nat) : Nat :=
  match n with
  | none => 4

throws an error.

reassigning to maintainer @eric-wieser since most of the code is in the meta part of the library which I'm not familiar with.

Thanks @JovanGerb, indeed I must have been remembering the behavior of let.

@kmill, do you know if core has a preference here?

This pull request has conflicts, please merge master and resolve them.

This pull request has conflicts, please merge master and resolve them.

@eric-wieser I don't think core has any advice, though let some is a couple orders of magnitude more common than let .some. Seeing .some/.none for Option does give me pause, so the change seems reasonable to me.

bors r+

Pull request successfully merged into master.

Build succeeded:

• CI Success