Skip to content

Commit a892262

Browse files
committed
chore: update stage0
1 parent fdf5cc4 commit a892262

File tree

21 files changed

+11664
-5798
lines changed

21 files changed

+11664
-5798
lines changed

stage0/stdlib/Init.c

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

stage0/stdlib/Init/Data/Array/Basic.c

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

stage0/stdlib/Init/Notation.c

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

stage0/stdlib/Init/Tactics.c

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

stage0/stdlib/Init/TacticsExtra.c

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

stage0/stdlib/Lean/Attributes.c

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

stage0/stdlib/Lean/Compiler/IR/Basic.c

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/Lean/Data/Json.c

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

stage0/stdlib/Lean/Data/Json/Elab.c

Lines changed: 4715 additions & 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)