Labels

• awaiting-author

  Waiting for PR author to address issues
• awaiting-mathlib

  We should not merge this until we have a successful Mathlib build
• awaiting-review

  Waiting for someone to review the PR
• backport releases/v4.18.0
• backport releases/v4.19.0
• backport releases/v4.20.0
• breaks-mathlib

  This is not necessarily a blocker for merging: but there needs to be a plan
• bug

  Something isn't working
• builds-mathlib

  CI has verified that Mathlib builds against this PR
• changelog-compiler

  Compiler, runtime, and FFI
• changelog-doc

  Documentation
• changelog-lake

  Lake
• changelog-language

  Language features, tactics, and metaprograms
• changelog-library

  Library
• changelog-no

  Do not include this PR in the release changelog
• changelog-other
• changelog-pp

  Pretty printing
• changelog-server

  Language server, widgets, and IDE extensions
• changes-stage0

  Contains stage0 changes, merge manually using rebase
• chore
• closing soon

  This issue will be closed soon (<1 month) as it is missing essential features.
• dependencies

  Pull requests that update a dependency file
• depends on new code generator

  We are currently working on a new compiler (code generator) for Lean. This issue/PR is blocked by it
• documentation

  Documentation improvement
• elaboration

  Affects the elaborator
• enhancement

  New feature or request
• error message

  Error message produced by Lean is confusing or not informative
• feature

  missing feature
• fixed by new code generator

  We are currently working on a new compiler (code generator) for Lean. This issue is fixed by it.
• force-mathlib-ci