Skip to content

Commit 5cdaeac

Browse files
gebnerleodemoura
authored andcommitted
chore: update stage0
1 parent e605c54 commit 5cdaeac

File tree

106 files changed

+37648
-75651
lines changed

Some content is hidden

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

106 files changed

+37648
-75651
lines changed

stage0/src/Init/Prelude.lean

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

stage0/src/library/compiler/erase_irrelevant.cpp

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/stdlib/Init/Coe.c

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

0 commit comments

Comments
 (0)