max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-26 18:18:55 -07:00
parent 8f27848d82
commit 65be990bdf
4 changed files with 682 additions and 306 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
stage0/src/Lean/Parser/Do.lean generated
View file

@ -86,8 +86,8 @@ def doSeq := doSeqBracketed <|> doSeqIndent
@[builtinDoElemParser] def doLet := parser! "let " >> letDecl
def doId := parser! try (ident >> optType >> leftArrow) >> termParser
def doPat := parser! try (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
@[builtinDoElemParser] def doAssign := notFollowedBy "let " >> (doId <|> doPat)
@[builtinDoElemParser] def doHave := parser! "have " >> Term.haveDecl
@[builtinDoElemParser] def doLetArrow := parser! "let " >> (doId <|> doPat)
@[builtinDoElemParser] def doHave := parser! "have " >> Term.haveDecl
/-
In `do` blocks, we support `if` without an `else`. Thus, we use indentation to prevent examples such as
```

2
stage0/stdlib/CMakeLists.txt generated
View file

File diff suppressed because one or more lines are too long

29
stage0/stdlib/Init/Notation.c generated
View file

@ -1,29 +0,0 @@
// Lean compiler output
// Module: Init.Notation
// Imports: Init
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* initialize_Init(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Notation(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

953
stage0/stdlib/Lean/Parser/Do.c generated
View file

File diff suppressed because it is too large Load diff