Skip to content

Commit

Permalink
chore: update stage0
Browse files Browse the repository at this point in the history
  • Loading branch information
leodemoura committed Aug 7, 2021
1 parent a863f1b commit a0c2142
Show file tree
Hide file tree
Showing 59 changed files with 4,303 additions and 3,872 deletions.
3 changes: 3 additions & 0 deletions stage0/src/Init/Prelude.lean

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

8 changes: 8 additions & 0 deletions stage0/src/Lean/Elab/Syntax.lean

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

6 changes: 6 additions & 0 deletions stage0/src/Lean/Meta/Basic.lean

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

7 changes: 5 additions & 2 deletions stage0/src/Lean/MetavarContext.lean

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 4 additions & 0 deletions stage0/src/library/compiler/csimp.cpp

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

210 changes: 105 additions & 105 deletions stage0/stdlib/Lean/Data/JsonRpc.c

Large diffs are not rendered by default.

1,322 changes: 661 additions & 661 deletions stage0/stdlib/Lean/Data/Lsp/Basic.c

Large diffs are not rendered by default.

202 changes: 101 additions & 101 deletions stage0/stdlib/Lean/Data/Lsp/Capabilities.c

Large diffs are not rendered by default.

910 changes: 455 additions & 455 deletions stage0/stdlib/Lean/Data/Lsp/Diagnostics.c

Large diffs are not rendered by default.

800 changes: 400 additions & 400 deletions stage0/stdlib/Lean/Data/Lsp/Extra.c

Large diffs are not rendered by default.

466 changes: 233 additions & 233 deletions stage0/stdlib/Lean/Data/Lsp/InitShutdown.c

Large diffs are not rendered by default.

24 changes: 12 additions & 12 deletions stage0/stdlib/Lean/Data/Lsp/Ipc.c

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

0 comments on commit a0c2142

Please sign in to comment.