Skip to content

Commit 5e5421d

Browse files
nomeatanomeata
committed
chore: update stage0
1 parent e1506cd commit 5e5421d

File tree

9 files changed

+7966
-6476
lines changed

9 files changed

+7966
-6476
lines changed

‎stage0/src/stdlib_flags.h‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,5 @@
11
#include "util/options.h"
22

3-
// please update stage0
4-
53
// stage0 update needed for grind_annotated command
64
namespace lean {
75
options get_default_options() {

‎stage0/stdlib/Init/WF.c‎

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

‎stage0/stdlib/Lean/Compiler/InlineAttrs.c‎

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

0 commit comments

Comments
 (0)