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-12-15 21:26:15 -08:00
parent 85e0b4fdb0
commit dc01e79388
3 changed files with 31 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
stage0/src/Init/Notation.lean generated
View file

@ -195,15 +195,16 @@ syntax[changeWith] "change " term " with " term (location)? : tactic
syntax rwRule := ("←" <|> "<-")? term
syntax rwRuleSeq := "[" rwRule,+,? "]"
-- TODO: fix 100000 priorities
syntax[rewrite] "rewrite " rwRule (location)? : tactic
syntax[rewriteSeq, 1] "rewrite " rwRuleSeq (location)? : tactic
syntax[rewriteSeq, 100000] "rewrite " rwRuleSeq (location)? : tactic
syntax[erewrite] "erewrite " rwRule (location)? : tactic
syntax[erewriteSeq, 1] "erewrite " rwRuleSeq (location)? : tactic
syntax[erewriteSeq, 100000] "erewrite " rwRuleSeq (location)? : tactic
syntax[rw] "rw " rwRule (location)? : tactic
syntax[rwSeq, 1] "rw " rwRuleSeq (location)? : tactic
syntax[rwSeq, 100000] "rw " rwRuleSeq (location)? : tactic
syntax[erw] "erw " rwRule (location)? : tactic
syntax[erwSeq, 1] "erw " rwRuleSeq (location)? : tactic
syntax[erwSeq, 100000] "erw " rwRuleSeq (location)? : tactic
private def withCheapRefl (tac : Syntax) : MacroM Syntax :=
`(tactic| $tac; try (withReducible rfl))
@ -248,7 +249,7 @@ syntax[introMatch] "intro " matchAlts : tactic
syntax[existsIntro] "exists " term : tactic
/- We use a priority > 0, to avoid ambiguity with the builtin `have` notation -/
macro[1] "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
macro[100000] "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
syntax "repeat " tacticSeq : tactic
macro_rules

4
stage0/src/Lean/Elab/Syntax.lean generated
View file

@ -231,12 +231,12 @@ where
private def elabKindPrio (stx : Syntax) (catName : Name) : CommandElabM (Option Name × Nat) := do
if stx.isNone then
pure (none, 0)
pure (none, evalPrio! default)
else
let arg := stx[1]
if arg.getKind == `Lean.Parser.Command.parserKind then
let k := arg[0].getId
pure (k, 0)
pure (k, evalPrio! default)
else if arg.getKind == `Lean.Parser.Command.parserPrio then
let prio ← liftMacroM <| evalPrio arg[0]
pure (none, prio)

45
stage0/stdlib/Lean/Elab/Syntax.c generated
View file

@ -443,7 +443,7 @@ lean_object* l_List_filterMap___at_Lean_Elab_Term_toParserDescrAux___spec__10(le
lean_object* l_Lean_Elab_Term_toParserDescrAux_match__5___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_String_capitalize(lean_object*);
lean_object* l___private_Lean_Elab_Util_0__Lean_Elab_expandMacro_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190_(lean_object*);
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192_(lean_object*);
lean_object* l_Lean_Elab_Command_elabSyntax_match__2___rarg(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_expandMixfix___lambda__1___closed__4;
extern lean_object* l_stx___x3c_x7c_x3e_____closed__6;
@ -1043,7 +1043,7 @@ lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___bo
lean_object* l___private_Init_Meta_0__Array_mapSepElemsMAux___at_Lean_Elab_Command_elabMacroRulesAux___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Subarray_forInUnsafe_loop___at___private_Lean_Elab_Syntax_0__Lean_Elab_Term_mkParserSeq___spec__1___closed__8;
extern lean_object* l_Lean_Elab_Term_expandFunBinders_loop___closed__4;
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190____closed__1;
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192____closed__1;
lean_object* l_Lean_Elab_Command_mkSimpleDelab_go___closed__4;
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_checkLeftRec___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_expandMacro___closed__2;
@ -13432,7 +13432,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = lean_unsigned_to_nat(0u);
x_2 = lean_unsigned_to_nat(1000u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
@ -13937,7 +13937,7 @@ return x_160;
}
else
{
lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166;
lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166; lean_object* x_167;
lean_dec(x_9);
lean_dec(x_3);
x_161 = lean_unsigned_to_nat(0u);
@ -13947,24 +13947,25 @@ x_163 = l_Lean_Syntax_getId(x_162);
lean_dec(x_162);
x_164 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_164, 0, x_163);
x_165 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_165, 0, x_164);
lean_ctor_set(x_165, 1, x_161);
x_165 = lean_unsigned_to_nat(1000u);
x_166 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_166, 0, x_165);
lean_ctor_set(x_166, 1, x_5);
return x_166;
lean_ctor_set(x_166, 0, x_164);
lean_ctor_set(x_166, 1, x_165);
x_167 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_167, 0, x_166);
lean_ctor_set(x_167, 1, x_5);
return x_167;
}
}
else
{
lean_object* x_167; lean_object* x_168;
lean_object* x_168; lean_object* x_169;
lean_dec(x_3);
x_167 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed__4;
x_168 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_168, 0, x_167);
lean_ctor_set(x_168, 1, x_5);
return x_168;
x_168 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed__4;
x_169 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_169, 0, x_168);
lean_ctor_set(x_169, 1, x_5);
return x_169;
}
}
}
@ -35042,7 +35043,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190____closed__1() {
static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -35052,11 +35053,11 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190_(lean_object* x_1) {
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190____closed__1;
x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192____closed__1;
x_3 = l_Lean_registerTraceClass(x_2, x_1);
return x_3;
}
@ -40142,9 +40143,9 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabMacro___closed__1);
res = l___regBuiltin_Lean_Elab_Command_elabMacro(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190____closed__1();
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190____closed__1);
res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19190_(lean_io_mk_world());
l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192____closed__1();
lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192____closed__1);
res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Syntax___hyg_19192_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Command_withExpectedType___closed__1 = _init_l_Lean_Elab_Command_withExpectedType___closed__1();