Skip to content

Commit 757a56a

Browse files
committed
chore: update stage0
1 parent 65ffb15 commit 757a56a

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

58 files changed

+8081
-1431
lines changed

stage0/src/Init/Core.lean

Lines changed: 1 addition & 1 deletion
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

stage0/src/Init/SizeOf.lean

Lines changed: 35 additions & 26 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

stage0/src/Lean/Declaration.lean

Lines changed: 39 additions & 36 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

stage0/src/Lean/Elab/Binders.lean

Lines changed: 1 addition & 1 deletion
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

stage0/src/Lean/Elab/BuiltinNotation.lean

Lines changed: 1 addition & 1 deletion
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

stage0/src/Lean/Elab/Command.lean

Lines changed: 1 addition & 1 deletion
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

stage0/src/Lean/Elab/Declaration.lean

Lines changed: 4 additions & 4 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

stage0/src/Lean/Elab/Deriving.lean

Lines changed: 1 addition & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

stage0/src/Lean/Elab/Deriving/BEq.lean

Lines changed: 5 additions & 5 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

stage0/src/Lean/Elab/Deriving/DecEq.lean

Lines changed: 4 additions & 4 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

0 commit comments

Comments
 (0)