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 2021-04-05 17:49:00 -07:00
parent 9fa89a73df
commit f9d5c4fc7c
9 changed files with 593 additions and 660 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
stage0/src/Init/Prelude.lean generated
View file

@ -1722,6 +1722,20 @@ def getNumArgs (stx : Syntax) : Nat :=
| Syntax.node _ args => args.size
| _ => 0
def isMissing : Syntax → Bool
| Syntax.missing => true
| _ => false
def isNodeOf (stx : Syntax) (k : SyntaxNodeKind) (n : Nat) : Bool :=
and (stx.isOfKind k) (beq stx.getNumArgs n)
/--
Similar to `isNodeOf`, but also succeeds if `stx` is `Syntax.missing`.
We use this function to implement `Syntax` pattern matching.
TODO: is this too liberal? -/
def isNodeOf' (stx : Syntax) (k : SyntaxNodeKind) (n : Nat) : Bool :=
or (stx.isNodeOf k n) stx.isMissing
def setArgs (stx : Syntax) (args : Array Syntax) : Syntax :=
match stx with
| node k _ => node k args

2
stage0/src/Lean/Elab/Quotation.lean generated
View file

@ -373,7 +373,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
uncovered,
doMatch := fun yes no => do
let cond ← match kind with
| `null => `(and (Syntax.isOfKind discr $(quote kind)) (BEq.beq (Array.size (Syntax.getArgs discr)) $(quote argPats.size)))
| `null => `(Syntax.isNodeOf' discr $(quote kind) $(quote argPats.size)) -- `isNodeOf'` also succeeds if discr is `Syntax.missing`, use `isNodeOf` to disable this
| `ident => `(and (Syntax.isIdent discr) (BEq.beq (Syntax.getId discr) $(quote quoted.getId)))
| _ => `(Syntax.isOfKind discr $(quote kind))
let newDiscrs ← (List.range argPats.size).mapM fun i => `(Syntax.getArg discr $(quote i))

2
stage0/src/Lean/Parser/Basic.lean generated
View file

@ -628,7 +628,7 @@ private partial def sepByFnAux (p : ParserFn) (sep : ParserFn) (allowTrailingSep
let mut s := p c s
if s.hasError then
if s.pos > pos then
return s
return s.mkNode nullKind iniSz
else if pOpt then
let s := s.restore sz pos
return s.mkNode nullKind iniSz

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

@ -14,10 +14,6 @@ def SourceInfo.updateTrailing (trailing : Substring) : SourceInfo → SourceInfo
/- Syntax AST -/
def Syntax.isMissing : Syntax → Bool
| Syntax.missing => true
| _ => false
inductive IsNode : Syntax → Prop where
| mk (kind : SyntaxNodeKind) (args : Array Syntax) : IsNode (Syntax.node kind args)

131
stage0/stdlib/Init/Prelude.c generated
View file

@ -247,6 +247,7 @@ lean_object* l_instInhabitedArrow__1___rarg(lean_object*);
lean_object* l_instMonadExcept(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind___closed__1;
lean_object* l_Lean_PrettyPrinter_instMonadQuotationUnexpandM___lambda__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isNodeOf_x27___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_instMonadLiftReaderT(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Macro_throwErrorAt___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_monadFunctorRefl___rarg(lean_object*, lean_object*);
@ -416,6 +417,7 @@ lean_object* l_Lean_replaceRef_match__1___rarg(lean_object*, lean_object*, lean_
lean_object* l_Array_getOp(lean_object*);
lean_object* l_Lean_numLitKind___closed__2;
lean_object* l_Lean_Macro_instMonadRefMacroM___closed__4;
lean_object* l_Lean_Syntax_isMissing___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_instMonadQuotationUnexpandM___closed__2;
lean_object* l_Unit_unit;
lean_object* l___private_Init_Prelude_0__Lean_simpMacroScopesAux(lean_object*);
@ -437,6 +439,7 @@ lean_object* l_throwThe(lean_object*, lean_object*);
lean_object* l_instMonadExcept___rarg(lean_object*);
lean_object* l_instMonadStateOf___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_instHMod___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isMissing_match__1(lean_object*);
lean_object* l_decEq___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_interpolatedStrKind___closed__2;
lean_object* l_inferInstance(lean_object*);
@ -478,6 +481,7 @@ lean_object* l_namedPattern___boxed(lean_object*, lean_object*);
uint8_t l_or(uint8_t, uint8_t);
lean_object* l_instInhabitedExcept(lean_object*, lean_object*);
lean_object* l_Monad_map___default(lean_object*);
uint8_t l_Lean_Syntax_isNodeOf_x27(lean_object*, lean_object*, lean_object*);
lean_object* l_instBEq(lean_object*);
lean_object* l_Nat_add___boxed(lean_object*, lean_object*);
lean_object* l_UInt64_ofNatCore___boxed(lean_object*, lean_object*);
@ -525,10 +529,13 @@ lean_object* l_instHShiftRight(lean_object*);
lean_object* l_Eq_ndrec___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkAtomFrom(lean_object*, lean_object*);
lean_object* l_and___boxed(lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNodeOf(lean_object*, lean_object*, lean_object*);
lean_object* l_instMonadReaderOf(lean_object*, lean_object*, lean_object*);
lean_object* l_EStateM_seqRight(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Eq_ndrec(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isMissing_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_instHasLessEqNat;
uint8_t l_Lean_Syntax_isMissing(lean_object*);
lean_object* l_EStateM_throw___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_setArg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_instMonadReaderT___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -557,6 +564,7 @@ lean_object* l_Lean_Macro_instMonadQuotationMacroM___closed__3;
lean_object* l_Fin_decLt(lean_object*);
lean_object* l_tryCatchThe___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_instHSub___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isNodeOf___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getNumArgs(lean_object*);
lean_object* l_instMonadWithReader(lean_object*, lean_object*);
lean_object* l_EStateM_instMonadEStateM___closed__3;
@ -8581,6 +8589,129 @@ lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Syntax_isMissing_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_4; lean_object* x_5;
lean_dec(x_3);
x_4 = lean_box(0);
x_5 = lean_apply_1(x_2, x_4);
return x_5;
}
else
{
lean_object* x_6;
lean_dec(x_2);
x_6 = lean_apply_1(x_3, x_1);
return x_6;
}
}
}
lean_object* l_Lean_Syntax_isMissing_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Syntax_isMissing_match__1___rarg), 3, 0);
return x_2;
}
}
uint8_t l_Lean_Syntax_isMissing(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
uint8_t x_2;
x_2 = 1;
return x_2;
}
else
{
uint8_t x_3;
x_3 = 0;
return x_3;
}
}
}
lean_object* l_Lean_Syntax_isMissing___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Syntax_isMissing(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
uint8_t l_Lean_Syntax_isNodeOf(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
lean_inc(x_1);
x_4 = l_Lean_Syntax_isOfKind(x_1, x_2);
if (x_4 == 0)
{
uint8_t x_5;
lean_dec(x_1);
x_5 = 0;
return x_5;
}
else
{
lean_object* x_6; uint8_t x_7;
x_6 = l_Lean_Syntax_getNumArgs(x_1);
lean_dec(x_1);
x_7 = lean_nat_dec_eq(x_6, x_3);
lean_dec(x_6);
return x_7;
}
}
}
lean_object* l_Lean_Syntax_isNodeOf___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = l_Lean_Syntax_isNodeOf(x_1, x_2, x_3);
lean_dec(x_3);
lean_dec(x_2);
x_5 = lean_box(x_4);
return x_5;
}
}
uint8_t l_Lean_Syntax_isNodeOf_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
lean_inc(x_1);
x_4 = l_Lean_Syntax_isNodeOf(x_1, x_2, x_3);
if (x_4 == 0)
{
uint8_t x_5;
x_5 = l_Lean_Syntax_isMissing(x_1);
lean_dec(x_1);
return x_5;
}
else
{
uint8_t x_6;
lean_dec(x_1);
x_6 = 1;
return x_6;
}
}
}
lean_object* l_Lean_Syntax_isNodeOf_x27___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_5;
x_4 = l_Lean_Syntax_isNodeOf_x27(x_1, x_2, x_3);
lean_dec(x_3);
lean_dec(x_2);
x_5 = lean_box(x_4);
return x_5;
}
}
lean_object* l_Lean_Syntax_setArgs(lean_object* x_1, lean_object* x_2) {
_start:
{

937
stage0/stdlib/Lean/Elab/Quotation.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -715,7 +715,7 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_1346____closed__1;
uint8_t l_Lean_Name_isAnonymous(lean_object*);
extern lean_object* l_Lean_Parser_Command_infix___elambda__1___closed__2;
lean_object* l_Lean_Elab_toAttributeKind___at_Lean_Elab_Command_expandNotation___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927_(uint8_t, uint8_t);
uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929_(uint8_t, uint8_t);
lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Term_withNestedParser___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Command_elabMacroRulesAux___spec__3(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_checkLeftRec(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -4039,7 +4039,7 @@ lean_inc(x_15);
lean_dec(x_13);
x_60 = lean_ctor_get_uint8(x_2, sizeof(void*)*1 + 2);
x_61 = 0;
x_62 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927_(x_60, x_61);
x_62 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929_(x_60, x_61);
if (x_62 == 0)
{
uint8_t x_63;

98
stage0/stdlib/Lean/Parser/Basic.c generated
View file

@ -92,7 +92,6 @@ lean_object* l_Lean_Parser_FirstTokens_toOptional_match__1(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_Lean_fieldIdxKind___closed__2;
lean_object* l_Lean_Parser_strAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7225____closed__1;
uint8_t l_USize_decEq(size_t, size_t);
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* l_Lean_Parser_eoi;
@ -174,6 +173,7 @@ lean_object* l_Lean_Parser_tokenWithAntiquotFn(lean_object*, lean_object*, lean_
lean_object* l_Lean_Parser_nonReservedSymbolInfo___closed__2;
lean_object* l_Lean_Parser_anyOfFn_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_strAux_parse(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929__match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Parser_isLitKind(lean_object*);
lean_object* l_Lean_Parser_instBEqError___closed__1;
extern lean_object* l_Lean_fieldIdxKind___closed__1;
@ -200,7 +200,6 @@ lean_object* l_Lean_Parser_withAntiquotSuffixSpliceFn___lambda__2(lean_object*,
lean_object* l_Lean_Parser_instInhabitedParserInfo___closed__1;
lean_object* l_Lean_Parser_nameLitNoAntiquot___closed__1;
lean_object* l_Lean_Parser_leadingParserAux___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207____closed__1;
uint8_t lean_name_eq(lean_object*, lean_object*);
uint8_t l_Lean_Parser_hexNumberFn___lambda__1(uint32_t);
lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1(lean_object*, lean_object*);
@ -209,6 +208,7 @@ lean_object* l_Lean_Parser_mkTokenAndFixPos___closed__2;
lean_object* l_Lean_Parser_mkAntiquot___closed__9;
uint8_t l_Lean_Parser_octalNumberFn___lambda__1(uint32_t);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_sepByFnAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209____closed__1;
lean_object* l_Lean_isIdRest___boxed(lean_object*);
lean_object* l_Lean_Parser_pushNone___elambda__1___boxed(lean_object*);
lean_object* l_Lean_Parser_notFollowedByFn(lean_object*, lean_object*, lean_object*, lean_object*);
@ -225,13 +225,13 @@ lean_object* lean_array_get_size(lean_object*);
lean_object* l_Std_PersistentHashMap_getCollisionNodeSize___rarg(lean_object*);
extern lean_object* l_Lean_charLitKind___closed__1;
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929____boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_tokenFn(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_withoutForbidden___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAtomicInfo(lean_object*);
lean_object* l_Lean_Parser_notFollowedBy(lean_object*, lean_object*);
lean_object* lean_string_utf8_extract(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Parser_info___default___closed__1;
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927____boxed(lean_object*, lean_object*);
uint8_t l_Char_isWhitespace(uint32_t);
lean_object* l_Lean_Parser_Error_merge_match__1(lean_object*);
lean_object* l_Lean_Parser_atomicFn(lean_object*, lean_object*, lean_object*);
@ -297,7 +297,6 @@ lean_object* l_Lean_Parser_orelseFnCore_match__1___rarg(lean_object*, lean_objec
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Parser_indexed___rarg(lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__6(lean_object*);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927__match__1___rarg(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
uint32_t l_Lean_Parser_getNext(lean_object*, lean_object*);
lean_object* l_List_toStringAux___at_Lean_Parser_FirstTokens_toStr___spec__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_andthenInfo___elambda__2(lean_object*, lean_object*, lean_object*);
@ -315,6 +314,7 @@ lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__3;
lean_object* l_Lean_Parser_instInhabitedParserCategory;
lean_object* l_Lean_Parser_scientificLitFn___closed__1;
lean_object* l_Lean_Parser_setExpectedFn_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209____lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_rawIdentFn(lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAntiquotSplice___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_insert___at_Lean_Parser_SyntaxNodeKindSet_insert___spec__1(lean_object*, lean_object*, lean_object*);
@ -323,7 +323,6 @@ lean_object* l_Lean_Parser_scientificLitNoAntiquot___closed__3;
lean_object* l_Lean_Parser_indexed(lean_object*);
lean_object* l_Lean_Parser_setExpectedFn___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAntiquotSplice___closed__9;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207____lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* lean_string_utf8_next(lean_object*, lean_object*);
lean_object* l_Lean_Parser_invalidLongestMatchParser(lean_object*);
lean_object* l_Lean_Parser_invalidLongestMatchParser___closed__1;
@ -377,7 +376,6 @@ lean_object* l_Lean_Parser_strLitFn___closed__1;
lean_object* l_Lean_Parser_Error_instToStringError;
lean_object* l_Lean_Parser_orelseFnCore_match__1(lean_object*);
lean_object* l_Lean_Parser_strLitFn___closed__2;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207____lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_evalParserConst___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_FirstTokens_instToStringFirstTokens___closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
@ -450,9 +448,9 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Syntax_foldArgsM___spec__1___ra
lean_object* l_Lean_Parser_ParserState_keepNewError(lean_object*, lean_object*);
lean_object* l_Lean_Parser_antiquotExpr;
lean_object* l_Lean_Parser_instInhabitedParserCategory___closed__1;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7225____lambda__1(lean_object*);
uint8_t l_Substring_contains(lean_object*, uint32_t);
lean_object* l_Lean_Parser_symbol(lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7227____lambda__1(lean_object*);
lean_object* l_Lean_Parser_isQuotableCharDefault___boxed(lean_object*);
lean_object* l_List_toStringAux___at_Lean_Parser_dbgTraceStateFn___spec__2(uint8_t, lean_object*);
lean_object* l_Lean_Parser_checkLineEqFn(lean_object*, lean_object*, lean_object*);
@ -504,6 +502,7 @@ lean_object* l_Lean_Parser_charLitNoAntiquot___closed__2;
lean_object* l_Lean_Parser_longestMatchStep(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_instAndThenParser;
lean_object* l_Lean_Parser_tryAnti_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7227____closed__1;
lean_object* l_Lean_Parser_setExpectedFn(lean_object*);
lean_object* l_List_eraseRepsAux___at_Lean_Parser_Error_toString___spec__4(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_strLitFn(lean_object*, lean_object*);
@ -559,7 +558,6 @@ lean_object* l_Lean_Parser_setExpectedFn_match__1(lean_object*);
lean_object* l_Lean_Parser_sepBy___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_pushNone___elambda__1___rarg(lean_object*);
lean_object* l_Lean_Parser_scientificLitFn(lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927__match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_to_list(lean_object*, lean_object*);
lean_object* l_Lean_Parser_PrattParsingTables_leadingParsers___default;
lean_object* l_Lean_Parser_fieldIdx___closed__5;
@ -764,6 +762,7 @@ lean_object* l_Std_RBNode_insert___at_Lean_Parser_TokenMap_insert___spec__5___ra
lean_object* l_Lean_Parser_ParserState_mkUnexpectedErrorAt(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_find___at_Lean_Parser_TokenMap_insert___spec__1(lean_object*);
lean_object* l_Lean_Parser_mergeOrElseErrors(lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209____lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__1(lean_object*);
lean_object* l_Lean_Parser_withPosition___lambda__1(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
@ -792,7 +791,7 @@ lean_object* l_Lean_Parser_Error_instToStringError___closed__1;
lean_object* l_Lean_Parser_checkTailNoWs_match__1(lean_object*);
lean_object* l_Lean_Parser_TokenMap_instEmptyCollectionTokenMap(lean_object*);
lean_object* l_Lean_Parser_orelseInfo___elambda__1(lean_object*, lean_object*, lean_object*);
uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927_(uint8_t, uint8_t);
uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929_(uint8_t, uint8_t);
extern lean_object* l_Array_instToStringArray___rarg___closed__1;
lean_object* l_Lean_Parser_errorAtSavedPos(lean_object*, uint8_t);
lean_object* l_Lean_Parser_mkAntiquot___closed__14;
@ -920,8 +919,8 @@ extern lean_object* l_Lean_Syntax_antiquotSpliceKind_x3f_match__1___rarg___close
lean_object* l_Lean_Parser_mkAntiquot___closed__6;
lean_object* l_Lean_Parser_parserOfStackFnUnsafe___closed__1;
extern lean_object* l_Lean_Syntax_mkAntiquotNode___closed__6;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207_(lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7225_(lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209_(lean_object*);
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7227_(lean_object*);
uint8_t l_Lean_Parser_instInhabitedLeadingIdentBehavior;
lean_object* l_Lean_Parser_fieldIdx___closed__7;
lean_object* l_Lean_Parser_mkAntiquot(lean_object*, lean_object*, uint8_t);
@ -955,6 +954,7 @@ lean_object* l_Lean_Parser_manyFn(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_ParserState_next___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkOptionalNode___closed__2;
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_Error_expectedToString_match__1(lean_object*);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929__match__1___rarg(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_updateCache_match__1(lean_object*);
lean_object* l_Lean_Parser_eoiFn___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_satisfySymbolFn_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -1027,13 +1027,13 @@ uint8_t lean_string_utf8_at_end(lean_object*, lean_object*);
lean_object* l_Lean_Parser_ParserState_replaceLongest___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_longestMatchStep___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_quotedCharCoreFn___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927__match__1(lean_object*);
lean_object* l_Lean_Parser_Error_toString___closed__1;
lean_object* l_Lean_Parser_instInhabitedParserInfo___lambda__1(lean_object*);
lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__2___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkAntiquot___closed__2;
lean_object* l_Lean_Parser_withResultOfInfo(lean_object*);
lean_object* l_Lean_Parser_withAntiquotSuffixSpliceFn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929__match__1(lean_object*);
lean_object* l_Lean_Parser_categoryParserOfStack___elambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_qpartition_loop___at_Lean_Parser_Error_toString___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_identFn(lean_object*, lean_object*);
@ -1046,10 +1046,10 @@ lean_object* l_Lean_Parser_antiquotExpr___closed__3;
lean_object* l_Lean_Parser_charLitNoAntiquot;
lean_object* l_Lean_Parser_FirstTokens_merge_match__1(lean_object*);
lean_object* l_Lean_mkErrorStringWithPos(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207____spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_isToken_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_unicodeSymbolFnAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_formatStxAux(lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209____spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_indexed_match__3(lean_object*);
lean_object* l_Lean_Parser_checkColGtFn___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_dbgTraceStateFn(lean_object*, lean_object*, lean_object*, lean_object*);
@ -8167,19 +8167,21 @@ return x_23;
}
else
{
lean_object* x_24; lean_object* x_25;
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_4);
return x_11;
x_24 = l_Lean_nullKind;
x_25 = l_Lean_Parser_ParserState_mkNode(x_11, x_24, x_4);
return x_25;
}
}
else
{
lean_object* x_24; lean_object* x_25;
lean_object* x_26; lean_object* x_27;
lean_dec(x_10);
x_24 = lean_box(0);
x_25 = l___private_Lean_Parser_Basic_0__Lean_Parser_sepByFnAux_parse___lambda__5(x_2, x_6, x_1, x_3, x_4, x_9, x_11, x_24);
return x_25;
x_26 = lean_box(0);
x_27 = l___private_Lean_Parser_Basic_0__Lean_Parser_sepByFnAux_parse___lambda__5(x_2, x_6, x_1, x_3, x_4, x_9, x_11, x_26);
return x_27;
}
}
}
@ -26869,7 +26871,7 @@ x_1 = 0;
return x_1;
}
}
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927__match__1___rarg(uint8_t x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929__match__1___rarg(uint8_t x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
switch (x_1) {
@ -26951,15 +26953,15 @@ return x_24;
}
}
}
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927__match__1(lean_object* x_1) {
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929__match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927__match__1___rarg___boxed), 6, 0);
x_2 = lean_alloc_closure((void*)(l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929__match__1___rarg___boxed), 6, 0);
return x_2;
}
}
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927__match__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929__match__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
uint8_t x_7; uint8_t x_8; lean_object* x_9;
@ -26967,11 +26969,11 @@ x_7 = lean_unbox(x_1);
lean_dec(x_1);
x_8 = lean_unbox(x_2);
lean_dec(x_2);
x_9 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927__match__1___rarg(x_7, x_8, x_3, x_4, x_5, x_6);
x_9 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929__match__1___rarg(x_7, x_8, x_3, x_4, x_5, x_6);
return x_9;
}
}
uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927_(uint8_t x_1, uint8_t x_2) {
uint8_t l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929_(uint8_t x_1, uint8_t x_2) {
_start:
{
switch (x_1) {
@ -27032,7 +27034,7 @@ return x_11;
}
}
}
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927____boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929____boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; uint8_t x_4; uint8_t x_5; lean_object* x_6;
@ -27040,7 +27042,7 @@ x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = lean_unbox(x_2);
lean_dec(x_2);
x_5 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927_(x_3, x_4);
x_5 = l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929_(x_3, x_4);
x_6 = lean_box(x_5);
return x_6;
}
@ -27049,7 +27051,7 @@ static lean_object* _init_l_Lean_Parser_instBEqLeadingIdentBehavior___closed__1(
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6927____boxed), 2, 0);
x_1 = lean_alloc_closure((void*)(l___private_Lean_Parser_Basic_0__Lean_Parser_beqLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_6929____boxed), 2, 0);
return x_1;
}
}
@ -28311,7 +28313,7 @@ lean_dec(x_1);
return x_6;
}
}
lean_object* l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207____spec__1(lean_object* x_1, lean_object* x_2) {
lean_object* l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209____spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
@ -28336,7 +28338,7 @@ return x_7;
}
}
}
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207____lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209____lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
@ -28344,34 +28346,34 @@ x_4 = l_Lean_Parser_whitespace(x_2, x_3);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207____closed__1() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207____lambda__1___boxed), 3, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209____lambda__1___boxed), 3, 0);
return x_1;
}
}
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207_(lean_object* x_1) {
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207____closed__1;
x_3 = l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207____spec__1(x_2, x_1);
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209____closed__1;
x_3 = l_IO_mkRef___at_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209____spec__1(x_2, x_1);
return x_3;
}
}
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207____lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209____lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207____lambda__1(x_1, x_2, x_3);
x_4 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209____lambda__1(x_1, x_2, x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_4;
}
}
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7225____lambda__1(lean_object* x_1) {
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7227____lambda__1(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
@ -28397,19 +28399,19 @@ return x_7;
}
}
}
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7225____closed__1() {
static lean_object* _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7227____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7225____lambda__1), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7227____lambda__1), 1, 0);
return x_1;
}
}
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7225_(lean_object* x_1) {
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7227_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7225____closed__1;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7227____closed__1;
x_3 = l_Lean_EnvExtensionInterfaceUnsafe_registerExt___rarg(x_2, x_1);
return x_3;
}
@ -33417,16 +33419,16 @@ l_Lean_Parser_instInhabitedParserCategory___closed__1 = _init_l_Lean_Parser_inst
lean_mark_persistent(l_Lean_Parser_instInhabitedParserCategory___closed__1);
l_Lean_Parser_instInhabitedParserCategory = _init_l_Lean_Parser_instInhabitedParserCategory();
lean_mark_persistent(l_Lean_Parser_instInhabitedParserCategory);
l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207____closed__1);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7207_(lean_io_mk_world());
l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209____closed__1);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7209_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_Parser_categoryParserFnRef = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Parser_categoryParserFnRef);
lean_dec_ref(res);
l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7225____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7225____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7225____closed__1);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7225_(lean_io_mk_world());
l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7227____closed__1 = _init_l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7227____closed__1();
lean_mark_persistent(l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7227____closed__1);
res = l_Lean_Parser_initFn____x40_Lean_Parser_Basic___hyg_7227_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_Parser_categoryParserFnExtension = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Parser_categoryParserFnExtension);

61
stage0/stdlib/Lean/Syntax.c generated
View file

@ -181,7 +181,6 @@ lean_object* l_Lean_Syntax_getAtomVal_x21_match__1(lean_object*);
lean_object* l_Lean_Syntax_antiquotSuffixSplice_x3f___boxed(lean_object*);
lean_object* l_Lean_Syntax_instForInTopDownSyntax_loop___at_Lean_Syntax_reprint___spec__2___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mkAntiquotNode___closed__5;
lean_object* l_Lean_Syntax_isMissing___boxed(lean_object*);
lean_object* l_Lean_Syntax_antiquotSpliceKind_x3f___boxed(lean_object*);
lean_object* l_Lean_Syntax_setAtomVal_match__1(lean_object*);
lean_object* l___private_Lean_Syntax_0__Lean_Syntax_updateInfo_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -190,7 +189,6 @@ lean_object* l_Lean_Syntax_MonadTraverser_setCur(lean_object*);
lean_object* l_Lean_Syntax_MonadTraverser_goLeft___rarg___closed__1;
lean_object* l_Lean_SyntaxNode_modifyArgs(lean_object*, lean_object*);
lean_object* l_Lean_SyntaxNode_getArgs___boxed(lean_object*);
lean_object* l_Lean_Syntax_isMissing_match__1(lean_object*);
lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isQuot_match__1(lean_object*);
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__1___boxed(lean_object*);
@ -219,9 +217,7 @@ lean_object* l_Lean_Syntax_Traverser_fromSyntax(lean_object*);
lean_object* l_Lean_unreachIsNodeAtom(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mkAntiquotNode___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_replaceM_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isMissing_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mkAntiquotNode___closed__1;
uint8_t l_Lean_Syntax_isMissing(lean_object*);
lean_object* l_Lean_Syntax_replaceM___at_Lean_Syntax_updateLeading___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getQuotContent(lean_object*);
lean_object* l_Lean_SyntaxNode_getNumArgs(lean_object*);
@ -397,61 +393,6 @@ return x_2;
}
}
}
lean_object* l_Lean_Syntax_isMissing_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_4; lean_object* x_5;
lean_dec(x_3);
x_4 = lean_box(0);
x_5 = lean_apply_1(x_2, x_4);
return x_5;
}
else
{
lean_object* x_6;
lean_dec(x_2);
x_6 = lean_apply_1(x_3, x_1);
return x_6;
}
}
}
lean_object* l_Lean_Syntax_isMissing_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Syntax_isMissing_match__1___rarg), 3, 0);
return x_2;
}
}
uint8_t l_Lean_Syntax_isMissing(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
uint8_t x_2;
x_2 = 1;
return x_2;
}
else
{
uint8_t x_3;
x_3 = 0;
return x_3;
}
}
}
lean_object* l_Lean_Syntax_isMissing___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Syntax_isMissing(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* l_Lean_unreachIsNodeMissing(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -816,7 +757,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Syntax_getAtomVal_x21___closed__1;
x_2 = l_Lean_Syntax_getAtomVal_x21___closed__2;
x_3 = lean_unsigned_to_nat(68u);
x_3 = lean_unsigned_to_nat(64u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l_Lean_Syntax_getAtomVal_x21___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);