Skip to content

Commit ceda66a

Browse files
committed
chore: update-stage0
1 parent df9cde9 commit ceda66a

File tree

110 files changed

+11996
-11102
lines changed

Some content is hidden

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

110 files changed

+11996
-11102
lines changed

stage0/src/Init/Control/Lawful.lean

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

stage0/src/Init/Control/Reader.lean

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

stage0/src/Init/Data/Array/Basic.lean

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

stage0/src/Init/Data/Format.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/Init/Data/Format/Syntax.lean

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

stage0/src/Init/Data/Nat/Basic.lean

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

stage0/src/Init/Data/Range.lean

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

stage0/src/Init/Meta.lean

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

stage0/src/Init/Prelude.lean

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

stage0/src/Lean/Data/Lsp/Capabilities.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.

0 commit comments

Comments
 (0)