chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
74bac15c6f
commit
ba16094e63
20 changed files with 24136 additions and 23991 deletions
|
|
@ -381,15 +381,15 @@ private unsafe partial def toPreterm : Syntax → TermElabM Expr
|
|||
e ← toPreterm stx;
|
||||
pure $ lctx.mkLambda #[mkFVar n] e
|
||||
| `Lean.Parser.Term.let => do
|
||||
let ⟨n, val⟩ := show Name × Syntax from match (args.get! 1).getKind with
|
||||
| `Lean.Parser.Term.letIdDecl => ((args.get! 1).getIdAt 0, (args.get! 1).getArg 4)
|
||||
| `Lean.Parser.Term.letPatDecl => (((args.get! 1).getArg 0).getIdAt 0, (args.get! 1).getArg 3)
|
||||
| _ => unreachable!;
|
||||
let decl := args.get! 1;
|
||||
let n := if (decl.getArg 0).isIdent then (decl.getArg 0).getId else (decl.getArg 0).getIdAt 0;
|
||||
let val := decl.getArg 4;
|
||||
let body := args.get! 3;
|
||||
val ← toPreterm val;
|
||||
lctx ← getLCtx;
|
||||
let lctx := lctx.mkLetDecl n n exprPlaceholder val;
|
||||
adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $ do
|
||||
e ← toPreterm $ args.get! 3;
|
||||
e ← toPreterm $ body;
|
||||
pure $ lctx.mkLambda #[mkFVar n] e
|
||||
| `Lean.Parser.Term.let_core =>
|
||||
-- parser! "let_core " >> termParser >> ":=" >> termParser >> "; " >> termParser
|
||||
|
|
|
|||
|
|
@ -180,16 +180,18 @@ fun stx => do
|
|||
trace `Elab stx $ fun _ => d;
|
||||
withMacroExpansion stx d $ elabCommand d
|
||||
|
||||
@[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
| `(macro_rules $alts*) => do
|
||||
-- TODO: clean up with matchAlt quotation
|
||||
k ← match_syntax ((alts.get! 0).getArg 1).getArg 0 with
|
||||
def elabMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
|
||||
k ← match_syntax ((alts.get! 0).getArg 0).getArg 0 with
|
||||
| `(`($quot)) => pure quot.getKind
|
||||
| stx => throwUnsupportedSyntax;
|
||||
-- TODO: meaningful, unhygienic def name for selective macro `open`ing?
|
||||
`(@[macro $(Lean.mkIdent k)] def myMacro : Macro := fun stx => match_syntax stx with $alts* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
|
||||
| _ => throwUnsupportedSyntax
|
||||
-- TODO: meaningful, unhygienic def name for selective macro `open`ing?
|
||||
`(@[macro $(Lean.mkIdent k)] def myMacro : Macro := fun stx => match_syntax stx with $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
|
||||
|
||||
@[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
|
||||
adaptExpander $ fun stx => match_syntax stx with
|
||||
| `(macro_rules $alts:matchAlt*) => elabMacroRulesAux alts
|
||||
| `(macro_rules | $alts:matchAlt*) => elabMacroRulesAux alts
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
/- We just ignore Lean3 notation declaration commands. -/
|
||||
@[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure ()
|
||||
|
|
|
|||
|
|
@ -305,20 +305,18 @@ let type := expandOptType ref (decl.getArg 2);
|
|||
let val := decl.getArg 4;
|
||||
elabLetDeclAux ref n binders type val body expectedType?
|
||||
|
||||
/-
|
||||
@[builtinTermElab «let»] def elabLetDecl : TermElab :=
|
||||
fun stx expectedType? => match_syntax stx with
|
||||
| `(let $id $args* := $val; $body) =>
|
||||
| `(let $id:ident $args* := $val; $body) =>
|
||||
elabLetDeclAux stx id.getId args (mkHole stx) val body expectedType?
|
||||
| `(let $id $args* : $type := $val; $body) =>
|
||||
| `(let $id:ident $args* : $type := $val; $body) =>
|
||||
elabLetDeclAux stx id.getId args type val body expectedType?
|
||||
| `(let $id:id := $val; $body) => do
|
||||
-- HACK: support single Term.id pattern let (as produced by quotations) by translation to ident let for now
|
||||
let id := id.getArg 0;
|
||||
stx ← `(let $id:ident := $val; $body);
|
||||
stx ← `(let $id := $val; $body);
|
||||
elabTerm stx expectedType?
|
||||
| _ => throwUnsupportedSyntax
|
||||
-/
|
||||
|
||||
@[init] private def regTraceClasses : IO Unit := do
|
||||
registerTraceClass `Elab.let;
|
||||
|
|
|
|||
|
|
@ -1460,7 +1460,7 @@ private def noImmediateColon {k : ParserKind} : Parser k :=
|
|||
else s
|
||||
}
|
||||
|
||||
private def pushNone {k : ParserKind} : Parser k :=
|
||||
def pushNone {k : ParserKind} : Parser k :=
|
||||
{ fn := fun a c s => s.pushSyntax mkNullNode }
|
||||
|
||||
/-
|
||||
|
|
@ -1490,6 +1490,9 @@ node kind $ try $ dollarSymbol >> checkNoWsBefore "no space before" >> antiquotE
|
|||
/- End of Antiquotations -/
|
||||
/- ===================== -/
|
||||
|
||||
def nodeWithAntiquot {k : ParserKind} (name : String) (kind : SyntaxNodeKind) (p : Parser k) : Parser k :=
|
||||
mkAntiquot name kind false <|> node kind p
|
||||
|
||||
def ident {k : ParserKind} : Parser k :=
|
||||
mkAntiquot "ident" identKind <|> identNoAntiquot
|
||||
|
||||
|
|
|
|||
|
|
@ -81,8 +81,8 @@ def simpleBinder := parser! many1 binderIdent
|
|||
@[builtinTermParser] def «forall» := parser! unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracktedBinder) >> ", " >> termParser
|
||||
|
||||
def matchAlt : Parser :=
|
||||
let k := `Lean.Parser.Term.matchAlt;
|
||||
mkAntiquot "matchAlt" k false <|> node k (sepBy1 termParser ", " >> darrow >> termParser)
|
||||
nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
|
||||
sepBy1 termParser ", " >> darrow >> termParser
|
||||
|
||||
def matchAlts (optionalFirstBar := true) : Parser :=
|
||||
withPosition $ fun pos =>
|
||||
|
|
@ -100,11 +100,11 @@ withPosition $ fun pos =>
|
|||
@[builtinTermParser] def «match_syntax» := parser! "match_syntax" >> termParser >> " with " >> matchAlts
|
||||
|
||||
/- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/
|
||||
def letIdLhs : Parser := ident >> checkWsBefore "expected space before binders" >> many bracktedBinder >> optType
|
||||
def letSimpleDecl : Parser := try (letIdLhs >> " := ") >> termParser
|
||||
def letPatDecl : Parser := try (termParser >> optType >> " := ") >> termParser
|
||||
def letEqnsDecl : Parser := letIdLhs >> matchAlts false
|
||||
def letDecl := letSimpleDecl <|> letPatDecl <|> letEqnsDecl
|
||||
def letIdLhs : Parser := ident >> checkWsBefore "expected space before binders" >> many bracktedBinder >> optType
|
||||
def letIdDecl : Parser := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl $ try (letIdLhs >> " := ") >> termParser
|
||||
def letPatDecl : Parser := node `Lean.Parser.Term.letDecl $ try (termParser >> pushNone >> optType >> " := ") >> termParser
|
||||
def letEqnsDecl : Parser := node `Lean.Parser.Term.letDecl $ letIdLhs >> matchAlts false
|
||||
def letDecl := letIdDecl <|> letPatDecl <|> letEqnsDecl
|
||||
@[builtinTermParser] def «let» := parser! "let " >> letDecl >> "; " >> termParser
|
||||
|
||||
@[builtinTermParser] def «let_core» := parser! "let_core " >> termParser >> ":=" >> termParser >> "; " >> termParser
|
||||
|
|
|
|||
|
|
@ -405,7 +405,6 @@ lean_object* l_Lean_Elab_Term_elabAnd___boxed(lean_object*, lean_object*, lean_o
|
|||
lean_object* l_Lean_Elab_Term_elabMap___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMap___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_elabGE___closed__2;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__5;
|
||||
lean_object* l_Lean_Elab_Term_elabMap___closed__2;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabGE___closed__2;
|
||||
|
|
@ -614,6 +613,7 @@ lean_object* l_Lean_Elab_Term_elabSubtype___lambda__1___closed__3;
|
|||
lean_object* l_Lean_Elab_Term_elabBEq___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_elabNe___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAnd___closed__3;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_elabSub___closed__3;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHave(lean_object*);
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabLE___closed__2;
|
||||
|
|
@ -939,7 +939,7 @@ x_70 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_71 = lean_array_push(x_70, x_69);
|
||||
x_72 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_73 = lean_array_push(x_71, x_72);
|
||||
x_74 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_74 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_75 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_75, 0, x_74);
|
||||
lean_ctor_set(x_75, 1, x_73);
|
||||
|
|
@ -1011,7 +1011,7 @@ x_113 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_114 = lean_array_push(x_113, x_112);
|
||||
x_115 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_116 = lean_array_push(x_114, x_115);
|
||||
x_117 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_117 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_118 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_118, 0, x_117);
|
||||
lean_ctor_set(x_118, 1, x_116);
|
||||
|
|
@ -1957,7 +1957,7 @@ x_122 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_123 = lean_array_push(x_122, x_121);
|
||||
x_124 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_125 = lean_array_push(x_123, x_124);
|
||||
x_126 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_126 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_127 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_127, 0, x_126);
|
||||
lean_ctor_set(x_127, 1, x_125);
|
||||
|
|
@ -2044,7 +2044,7 @@ x_173 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_174 = lean_array_push(x_173, x_172);
|
||||
x_175 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_176 = lean_array_push(x_174, x_175);
|
||||
x_177 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_177 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_178 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_178, 0, x_177);
|
||||
lean_ctor_set(x_178, 1, x_176);
|
||||
|
|
@ -2407,7 +2407,7 @@ x_43 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_44 = lean_array_push(x_43, x_42);
|
||||
x_45 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_46 = lean_array_push(x_44, x_45);
|
||||
x_47 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_47 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_48 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_48, 0, x_47);
|
||||
lean_ctor_set(x_48, 1, x_46);
|
||||
|
|
@ -2489,7 +2489,7 @@ x_92 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_93 = lean_array_push(x_92, x_91);
|
||||
x_94 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_95 = lean_array_push(x_93, x_94);
|
||||
x_96 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_96 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_97 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_97, 0, x_96);
|
||||
lean_ctor_set(x_97, 1, x_95);
|
||||
|
|
@ -2663,7 +2663,7 @@ x_168 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_169 = lean_array_push(x_168, x_167);
|
||||
x_170 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_171 = lean_array_push(x_169, x_170);
|
||||
x_172 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_172 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_173 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_173, 0, x_172);
|
||||
lean_ctor_set(x_173, 1, x_171);
|
||||
|
|
@ -2753,7 +2753,7 @@ x_221 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_222 = lean_array_push(x_221, x_220);
|
||||
x_223 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_224 = lean_array_push(x_222, x_223);
|
||||
x_225 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_225 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_226 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_226, 0, x_225);
|
||||
lean_ctor_set(x_226, 1, x_224);
|
||||
|
|
@ -3472,7 +3472,7 @@ x_33 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_34 = lean_array_push(x_33, x_32);
|
||||
x_35 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_36 = lean_array_push(x_34, x_35);
|
||||
x_37 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_37 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_38 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_38, 0, x_37);
|
||||
lean_ctor_set(x_38, 1, x_36);
|
||||
|
|
@ -3541,7 +3541,7 @@ x_73 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_74 = lean_array_push(x_73, x_72);
|
||||
x_75 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_76 = lean_array_push(x_74, x_75);
|
||||
x_77 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_77 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_78 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_78, 0, x_77);
|
||||
lean_ctor_set(x_78, 1, x_76);
|
||||
|
|
@ -3821,7 +3821,7 @@ x_45 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_46 = lean_array_push(x_45, x_44);
|
||||
x_47 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_48 = lean_array_push(x_46, x_47);
|
||||
x_49 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_49 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_50 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_50, 0, x_49);
|
||||
lean_ctor_set(x_50, 1, x_48);
|
||||
|
|
@ -3895,7 +3895,7 @@ x_89 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_90 = lean_array_push(x_89, x_88);
|
||||
x_91 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_92 = lean_array_push(x_90, x_91);
|
||||
x_93 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_93 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_94 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_94, 0, x_93);
|
||||
lean_ctor_set(x_94, 1, x_92);
|
||||
|
|
@ -4015,7 +4015,7 @@ x_150 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_151 = lean_array_push(x_150, x_149);
|
||||
x_152 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_153 = lean_array_push(x_151, x_152);
|
||||
x_154 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_154 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_155 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_155, 0, x_154);
|
||||
lean_ctor_set(x_155, 1, x_153);
|
||||
|
|
@ -4089,7 +4089,7 @@ x_194 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_195 = lean_array_push(x_194, x_193);
|
||||
x_196 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_197 = lean_array_push(x_195, x_196);
|
||||
x_198 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_198 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_199 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_199, 0, x_198);
|
||||
lean_ctor_set(x_199, 1, x_197);
|
||||
|
|
@ -4244,7 +4244,7 @@ x_266 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_267 = lean_array_push(x_266, x_265);
|
||||
x_268 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_269 = lean_array_push(x_267, x_268);
|
||||
x_270 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_270 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_271 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_271, 0, x_270);
|
||||
lean_ctor_set(x_271, 1, x_269);
|
||||
|
|
@ -4311,7 +4311,7 @@ x_305 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_306 = lean_array_push(x_305, x_304);
|
||||
x_307 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_308 = lean_array_push(x_306, x_307);
|
||||
x_309 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_309 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_310 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_310, 0, x_309);
|
||||
lean_ctor_set(x_310, 1, x_308);
|
||||
|
|
@ -4426,7 +4426,7 @@ x_363 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_364 = lean_array_push(x_363, x_362);
|
||||
x_365 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_366 = lean_array_push(x_364, x_365);
|
||||
x_367 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_367 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_368 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_368, 0, x_367);
|
||||
lean_ctor_set(x_368, 1, x_366);
|
||||
|
|
@ -4493,7 +4493,7 @@ x_402 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_403 = lean_array_push(x_402, x_401);
|
||||
x_404 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_405 = lean_array_push(x_403, x_404);
|
||||
x_406 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_406 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_407 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_407, 0, x_406);
|
||||
lean_ctor_set(x_407, 1, x_405);
|
||||
|
|
@ -5217,7 +5217,7 @@ x_94 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_95 = lean_array_push(x_94, x_93);
|
||||
x_96 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_97 = lean_array_push(x_95, x_96);
|
||||
x_98 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_98 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_99 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_99, 0, x_98);
|
||||
lean_ctor_set(x_99, 1, x_97);
|
||||
|
|
@ -5307,7 +5307,7 @@ x_141 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_142 = lean_array_push(x_141, x_140);
|
||||
x_143 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_144 = lean_array_push(x_142, x_143);
|
||||
x_145 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_145 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_146 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_146, 0, x_145);
|
||||
lean_ctor_set(x_146, 1, x_144);
|
||||
|
|
@ -5408,7 +5408,7 @@ x_193 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_194 = lean_array_push(x_193, x_192);
|
||||
x_195 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_196 = lean_array_push(x_194, x_195);
|
||||
x_197 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_197 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_198 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_198, 0, x_197);
|
||||
lean_ctor_set(x_198, 1, x_196);
|
||||
|
|
@ -5516,7 +5516,7 @@ x_250 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
|
|||
x_251 = lean_array_push(x_250, x_249);
|
||||
x_252 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
|
||||
x_253 = lean_array_push(x_251, x_252);
|
||||
x_254 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_254 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_255 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_255, 0, x_254);
|
||||
lean_ctor_set(x_255, 1, x_253);
|
||||
|
|
|
|||
|
|
@ -31,7 +31,6 @@ lean_object* l_PersistentHashMap_findAux___main___at_Lean_Elab_Command_elabComma
|
|||
extern lean_object* l_Lean_Meta_check___closed__1;
|
||||
lean_object* l_Lean_Syntax_isNatLitAux(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_getOptions(lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_27__BuiltinParserAttribute_add___closed__2;
|
||||
extern lean_object* l_Lean_Elab_Tactic_evalTactic___main___closed__3;
|
||||
extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__8;
|
||||
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabNamespace___closed__3;
|
||||
|
|
@ -325,7 +324,6 @@ extern lean_object* l_Lean_Parser_Command_open___elambda__1___closed__2;
|
|||
uint8_t l_Array_contains___at_Lean_findField_x3f___main___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_CommandElabM_MonadQuotation___closed__1;
|
||||
lean_object* l_Lean_Elab_mkElabAttribute___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_16__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
lean_object* l_Lean_Elab_Command_elabEnd___closed__2;
|
||||
lean_object* l_Lean_Elab_Command_elabCommand(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_liftIO___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -380,6 +378,7 @@ extern lean_object* l_Lean_Elab_declareBuiltinMacro___closed__4;
|
|||
lean_object* l___private_Init_Lean_Elab_Command_2__getState(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Command_universe___elambda__1___closed__2;
|
||||
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Elab_Command_elabCommand___main___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_15__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabOpen___closed__2;
|
||||
extern lean_object* l_Bool_HasRepr___closed__1;
|
||||
extern lean_object* l_Lean_Syntax_inhabited;
|
||||
|
|
@ -476,6 +475,7 @@ lean_object* l_Lean_Elab_Command_throwAlreadyDeclaredUniverseLevel___rarg(lean_o
|
|||
extern lean_object* l_Lean_Parser_Command_openOnly___elambda__1___closed__2;
|
||||
lean_object* l_Array_toList___rarg(lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_CommandElabM_monadLog___lambda__3(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_26__BuiltinParserAttribute_add___closed__2;
|
||||
lean_object* l_Lean_Elab_Command_setOption___closed__3;
|
||||
lean_object* l_Lean_Elab_Command_registerBuiltinCommandElabAttr___lambda__1___closed__5;
|
||||
lean_object* l___private_Init_Lean_Elab_Command_4__modifyGetState___rarg(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -3398,7 +3398,7 @@ x_27 = l_Lean_Name_toStringWithSep___main(x_26, x_1);
|
|||
x_28 = l_Lean_Elab_Command_addBuiltinCommandElab___closed__1;
|
||||
x_29 = lean_string_append(x_28, x_27);
|
||||
lean_dec(x_27);
|
||||
x_30 = l___private_Init_Lean_Parser_Parser_16__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
x_30 = l___private_Init_Lean_Parser_Parser_15__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
x_31 = lean_string_append(x_29, x_30);
|
||||
x_32 = lean_alloc_ctor(18, 1, 0);
|
||||
lean_ctor_set(x_32, 0, x_31);
|
||||
|
|
@ -3503,7 +3503,7 @@ x_52 = l_Lean_Name_toStringWithSep___main(x_51, x_1);
|
|||
x_53 = l_Lean_Elab_Command_addBuiltinCommandElab___closed__1;
|
||||
x_54 = lean_string_append(x_53, x_52);
|
||||
lean_dec(x_52);
|
||||
x_55 = l___private_Init_Lean_Parser_Parser_16__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
x_55 = l___private_Init_Lean_Parser_Parser_15__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
x_56 = lean_string_append(x_54, x_55);
|
||||
x_57 = lean_alloc_ctor(18, 1, 0);
|
||||
lean_ctor_set(x_57, 0, x_56);
|
||||
|
|
@ -3830,7 +3830,7 @@ lean_dec(x_13);
|
|||
lean_dec(x_11);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_25 = l___private_Init_Lean_Parser_Parser_27__BuiltinParserAttribute_add___closed__2;
|
||||
x_25 = l___private_Init_Lean_Parser_Parser_26__BuiltinParserAttribute_add___closed__2;
|
||||
x_26 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_26, 0, x_25);
|
||||
lean_ctor_set(x_26, 1, x_12);
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
|
|
@ -24,7 +24,6 @@ lean_object* l_Lean_Elab_Tactic_getLocalInsts___boxed(lean_object*, lean_object*
|
|||
lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Tactic_withMVarContext___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_PersistentHashMap_contains___at_Lean_Elab_Tactic_addBuiltinTactic___spec__4(lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_27__BuiltinParserAttribute_add___closed__2;
|
||||
lean_object* l_Lean_Elab_Tactic_evalTactic___main___closed__3;
|
||||
extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__8;
|
||||
lean_object* l_PersistentHashMap_find_x3f___at_Lean_Elab_Tactic_evalTactic___main___spec__2(lean_object*, lean_object*);
|
||||
|
|
@ -238,7 +237,6 @@ extern lean_object* l_Lean_Parser_Tactic_paren___elambda__1___closed__1;
|
|||
lean_object* l_Lean_Elab_Tactic_monadLog___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_ensureHasType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_mkElabAttribute___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_16__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
lean_object* l_Lean_Elab_Tactic_save___boxed(lean_object*);
|
||||
lean_object* l_Lean_Elab_Tactic_registerBuiltinTacticAttr___closed__5;
|
||||
lean_object* l_mkHashMapImp___rarg(lean_object*);
|
||||
|
|
@ -274,6 +272,7 @@ lean_object* l_Lean_Elab_Tactic_evalIntros___lambda__1(lean_object*, lean_object
|
|||
extern lean_object* l_Lean_Elab_declareBuiltinMacro___closed__4;
|
||||
lean_object* l_List_erase___main___at_Lean_Elab_Tactic_evalCase___spec__2(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_traceAtCmdPos___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_15__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
lean_object* l_Lean_Elab_Tactic_registerBuiltinTacticAttr___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Tactic_throwUnsupportedSyntax(lean_object*);
|
||||
lean_object* l_Lean_Elab_Tactic_registerBuiltinTacticAttr___lambda__1___closed__1;
|
||||
|
|
@ -366,6 +365,7 @@ lean_object* l_Lean_Elab_Tactic_EStateM_Backtrackable___closed__2;
|
|||
lean_object* l_Array_toList___rarg(lean_object*);
|
||||
lean_object* l_Lean_Elab_Tactic_ensureHasType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_26__BuiltinParserAttribute_add___closed__2;
|
||||
lean_object* l_Lean_Elab_Tactic_withMacroExpansion___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Tactic_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_reportUnsolvedGoals(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -3154,7 +3154,7 @@ x_27 = l_Lean_Name_toStringWithSep___main(x_26, x_1);
|
|||
x_28 = l_Lean_Elab_Tactic_addBuiltinTactic___closed__1;
|
||||
x_29 = lean_string_append(x_28, x_27);
|
||||
lean_dec(x_27);
|
||||
x_30 = l___private_Init_Lean_Parser_Parser_16__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
x_30 = l___private_Init_Lean_Parser_Parser_15__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
x_31 = lean_string_append(x_29, x_30);
|
||||
x_32 = lean_alloc_ctor(18, 1, 0);
|
||||
lean_ctor_set(x_32, 0, x_31);
|
||||
|
|
@ -3259,7 +3259,7 @@ x_52 = l_Lean_Name_toStringWithSep___main(x_51, x_1);
|
|||
x_53 = l_Lean_Elab_Tactic_addBuiltinTactic___closed__1;
|
||||
x_54 = lean_string_append(x_53, x_52);
|
||||
lean_dec(x_52);
|
||||
x_55 = l___private_Init_Lean_Parser_Parser_16__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
x_55 = l___private_Init_Lean_Parser_Parser_15__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
x_56 = lean_string_append(x_54, x_55);
|
||||
x_57 = lean_alloc_ctor(18, 1, 0);
|
||||
lean_ctor_set(x_57, 0, x_56);
|
||||
|
|
@ -3578,7 +3578,7 @@ lean_dec(x_13);
|
|||
lean_dec(x_11);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_25 = l___private_Init_Lean_Parser_Parser_27__BuiltinParserAttribute_add___closed__2;
|
||||
x_25 = l___private_Init_Lean_Parser_Parser_26__BuiltinParserAttribute_add___closed__2;
|
||||
x_26 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_26, 0, x_25);
|
||||
lean_ctor_set(x_26, 1, x_12);
|
||||
|
|
|
|||
|
|
@ -44,7 +44,6 @@ lean_object* l_Lean_Syntax_isNatLitAux(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Elab_Term_elabRawCharLit___closed__3;
|
||||
lean_object* l_PersistentArray_foldlMAux___main___at___private_Init_Lean_Elab_Term_3__fromMetaState___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabNum___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_27__BuiltinParserAttribute_add___closed__2;
|
||||
extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__8;
|
||||
lean_object* l_Lean_Elab_Term_State_inhabited;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabChar(lean_object*);
|
||||
|
|
@ -448,7 +447,6 @@ lean_object* l_Lean_Elab_Term_elabTermAux(lean_object*, uint8_t, lean_object*, l
|
|||
lean_object* l_Lean_Elab_Term_termElabAttribute___closed__5;
|
||||
lean_object* l_Lean_Elab_Term_ensureHasType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_mkElabAttribute___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_16__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabArrayLit___closed__3;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabArrayLit(lean_object*);
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSort___closed__1;
|
||||
|
|
@ -513,12 +511,12 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabRawNumLit___closed__1;
|
|||
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__10;
|
||||
lean_object* l_Lean_ConstantInfo_lparams(lean_object*);
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabNamedHole(lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_mkFreshAnonymousName(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_withLCtx(lean_object*);
|
||||
extern lean_object* l_Option_HasRepr___rarg___closed__3;
|
||||
lean_object* l_Lean_Elab_Term_traceAtCmdPos___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Elab_Term_elabTermAux___main___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_15__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_withoutPostponing___rarg(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__2;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabArrayLit___closed__1;
|
||||
|
|
@ -663,6 +661,7 @@ lean_object* l_Lean_Elab_Term_monadLog___closed__11;
|
|||
lean_object* l_Lean_Elab_Term_mkTacticMVar___closed__2;
|
||||
extern lean_object* l_Lean_Expr_Inhabited;
|
||||
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_26__BuiltinParserAttribute_add___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_addBuiltinTermElab(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__1;
|
||||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabStr(lean_object*);
|
||||
|
|
@ -797,6 +796,7 @@ lean_object* l___private_Init_Lean_Elab_Term_9__mkPairsAux___boxed(lean_object*,
|
|||
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabRawNumLit(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_mkTermElabAttribute___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_mkFreshInstanceName___rarg___closed__2;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
lean_object* l_Lean_mkApp3(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Expr_isSort(lean_object*);
|
||||
lean_object* l_Lean_Meta_decLevel_x3f(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -2741,7 +2741,7 @@ x_27 = l_Lean_Name_toStringWithSep___main(x_26, x_1);
|
|||
x_28 = l_Lean_Elab_Term_addBuiltinTermElab___closed__1;
|
||||
x_29 = lean_string_append(x_28, x_27);
|
||||
lean_dec(x_27);
|
||||
x_30 = l___private_Init_Lean_Parser_Parser_16__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
x_30 = l___private_Init_Lean_Parser_Parser_15__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
x_31 = lean_string_append(x_29, x_30);
|
||||
x_32 = lean_alloc_ctor(18, 1, 0);
|
||||
lean_ctor_set(x_32, 0, x_31);
|
||||
|
|
@ -2846,7 +2846,7 @@ x_52 = l_Lean_Name_toStringWithSep___main(x_51, x_1);
|
|||
x_53 = l_Lean_Elab_Term_addBuiltinTermElab___closed__1;
|
||||
x_54 = lean_string_append(x_53, x_52);
|
||||
lean_dec(x_52);
|
||||
x_55 = l___private_Init_Lean_Parser_Parser_16__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
x_55 = l___private_Init_Lean_Parser_Parser_15__throwParserCategoryAlreadyDefined___rarg___closed__2;
|
||||
x_56 = lean_string_append(x_54, x_55);
|
||||
x_57 = lean_alloc_ctor(18, 1, 0);
|
||||
lean_ctor_set(x_57, 0, x_56);
|
||||
|
|
@ -3173,7 +3173,7 @@ lean_dec(x_13);
|
|||
lean_dec(x_11);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_25 = l___private_Init_Lean_Parser_Parser_27__BuiltinParserAttribute_add___closed__2;
|
||||
x_25 = l___private_Init_Lean_Parser_Parser_26__BuiltinParserAttribute_add___closed__2;
|
||||
x_26 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_26, 0, x_25);
|
||||
lean_ctor_set(x_26, 1, x_12);
|
||||
|
|
@ -18384,7 +18384,7 @@ lean_object* l_Lean_Elab_Term_elabParen(lean_object* x_1, lean_object* x_2, lean
|
|||
_start:
|
||||
{
|
||||
uint8_t x_5; lean_object* x_147; uint8_t x_148;
|
||||
x_147 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_147 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
lean_inc(x_1);
|
||||
x_148 = l_Lean_Syntax_isOfKind(x_1, x_147);
|
||||
if (x_148 == 0)
|
||||
|
|
@ -18978,7 +18978,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabParen(lean_object* x_1) {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_3 = l___regBuiltinTermElab_Lean_Elab_Term_elabParen___closed__2;
|
||||
x_4 = l___regBuiltinTermElab_Lean_Elab_Term_elabParen___closed__3;
|
||||
x_5 = l_Lean_Elab_Term_addBuiltinTermElab(x_2, x_3, x_4, x_1);
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -25,7 +25,6 @@ lean_object* l___private_Init_Lean_Elab_Util_6__ElabAttribute_add___rarg___boxed
|
|||
extern lean_object* l_Lean_Macro_throwUnsupported___closed__1;
|
||||
extern lean_object* l___private_Init_Lean_Environment_8__persistentEnvExtensionsRef;
|
||||
lean_object* l_AssocList_contains___main___at_Lean_Elab_ElabFnTable_insert___spec__26___rarg___boxed(lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_27__BuiltinParserAttribute_add___closed__2;
|
||||
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
|
||||
lean_object* l_Lean_SMap_insert___at_Lean_Elab_ElabFnTable_insert___spec__20___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_mkMacroAttribute(lean_object*);
|
||||
|
|
@ -296,6 +295,7 @@ lean_object* l_Lean_SMap_insert___at_Lean_Elab_ElabFnTable_insert___spec__9(lean
|
|||
lean_object* l_PersistentHashMap_getCollisionNodeSize___rarg(lean_object*);
|
||||
lean_object* l_PersistentHashMap_empty___at_Lean_Elab_mkBuiltinMacroFnTable___spec__3;
|
||||
lean_object* l_mkHashMap___at_Lean_Elab_mkElabAttributeAux___spec__5___rarg(lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_26__BuiltinParserAttribute_add___closed__2;
|
||||
lean_object* l_Lean_Elab_declareBuiltinMacro___closed__8;
|
||||
lean_object* lean_mk_array(lean_object*, lean_object*);
|
||||
lean_object* l_PersistentHashMap_findAux___main___at_Lean_Elab_getMacros___spec__3(lean_object*, size_t, lean_object*);
|
||||
|
|
@ -5859,7 +5859,7 @@ lean_dec(x_13);
|
|||
lean_dec(x_11);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_25 = l___private_Init_Lean_Parser_Parser_27__BuiltinParserAttribute_add___closed__2;
|
||||
x_25 = l___private_Init_Lean_Parser_Parser_26__BuiltinParserAttribute_add___closed__2;
|
||||
x_26 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_26, 0, x_25);
|
||||
lean_ctor_set(x_26, 1, x_12);
|
||||
|
|
|
|||
|
|
@ -59,6 +59,7 @@ lean_object* l_Lean_Parser_Command_inductive___elambda__1(lean_object*, lean_obj
|
|||
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Command_attributes___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_stxQuot___closed__8;
|
||||
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Command_declId___elambda__1___spec__2(uint8_t, uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_Term_matchAlt___closed__3;
|
||||
lean_object* l_Lean_Parser_Command_structImplicitBinder___closed__2;
|
||||
lean_object* l_Lean_Parser_Command_extends___elambda__1___closed__7;
|
||||
lean_object* l_Lean_Parser_Command_end___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -103,7 +104,6 @@ lean_object* l_Lean_Parser_Command_openHiding;
|
|||
lean_object* l_Lean_Parser_Command_synth___elambda__1___closed__7;
|
||||
lean_object* l_Lean_Parser_Command_declModifiers___closed__8;
|
||||
lean_object* l_Lean_Parser_Command_def___elambda__1___closed__8;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
lean_object* l_Lean_Parser_regBuiltinCommandParserAttr___closed__4;
|
||||
lean_object* l_Lean_Parser_Command_partial___elambda__1___closed__7;
|
||||
lean_object* l_Lean_Parser_Command_export___closed__8;
|
||||
|
|
@ -652,6 +652,7 @@ lean_object* l_Lean_Parser_Command_abbrev___closed__8;
|
|||
lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_open___elambda__1___closed__8;
|
||||
lean_object* l_Lean_Parser_Command_classTk___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__2;
|
||||
lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Command_variable___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_optDeclSig___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -674,6 +675,7 @@ lean_object* l_Lean_Parser_Command_private___closed__2;
|
|||
lean_object* l_Lean_Parser_Command_open___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_openRenaming___elambda__1___closed__4;
|
||||
lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__12;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__6;
|
||||
lean_object* l_Lean_Parser_Command_declValSimple___closed__2;
|
||||
lean_object* l_Lean_Parser_Command_attributes___closed__4;
|
||||
lean_object* l_Lean_Parser_Command_export;
|
||||
|
|
@ -792,7 +794,6 @@ lean_object* l_Lean_Parser_Command_declVal___closed__3;
|
|||
lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__13;
|
||||
lean_object* l_Lean_Parser_Command_axiom___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Command_structCtor___closed__5;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__2;
|
||||
extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__9;
|
||||
lean_object* l_Lean_Parser_Command_docComment___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Command_private___closed__4;
|
||||
|
|
@ -833,6 +834,7 @@ lean_object* l_Lean_Parser_Command_attributes___elambda__1___closed__8;
|
|||
lean_object* l_Lean_Parser_Command_declaration___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_declSig___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_inductive___closed__1;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
lean_object* l_Lean_Parser_Command_declValSimple___closed__4;
|
||||
lean_object* l_Lean_Parser_Command_theorem___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_classInductive___elambda__1___closed__8;
|
||||
|
|
@ -852,7 +854,6 @@ lean_object* l_Lean_Parser_Command_introRule___closed__2;
|
|||
lean_object* l_Lean_Parser_Command_def___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_attrInstance___closed__3;
|
||||
lean_object* l_Lean_Parser_Command_export___elambda__1___closed__4;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_structure___closed__4;
|
||||
lean_object* l_Lean_Parser_Command_declModifiers___elambda__1___closed__1;
|
||||
extern lean_object* l_Lean_Parser_Term_explicitUniv___closed__1;
|
||||
|
|
@ -914,7 +915,6 @@ lean_object* l_Lean_Parser_Command_universes___elambda__1___closed__2;
|
|||
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Command_attributes___elambda__1___spec__2(uint8_t, uint8_t, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Command_classInductive___elambda__1___closed__9;
|
||||
lean_object* l_Lean_Parser_Command_openRenaming___closed__2;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__6;
|
||||
lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__9;
|
||||
lean_object* l_Lean_Parser_Command_declaration___closed__8;
|
||||
lean_object* l_Lean_Parser_Command_optDeclSig___elambda__1___closed__4;
|
||||
|
|
@ -947,7 +947,6 @@ lean_object* l_Lean_Parser_Command_structureTk___closed__5;
|
|||
lean_object* l_Lean_Parser_Command_universes___elambda__1___closed__9;
|
||||
extern lean_object* l_Lean_Parser_Term_doPat___elambda__1___closed__9;
|
||||
lean_object* l_Lean_Parser_Command_set__option___closed__1;
|
||||
extern lean_object* l_Lean_Parser_Term_matchAlt___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_protected___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Command_introRule___closed__5;
|
||||
lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__7;
|
||||
|
|
@ -1043,6 +1042,7 @@ lean_object* l_Lean_Parser_Command_init__quot;
|
|||
lean_object* l_Lean_Parser_Command_openRenaming___closed__6;
|
||||
lean_object* l_Lean_Parser_Command_axiom___elambda__1___closed__5;
|
||||
lean_object* l_Lean_Parser_Command_openHiding___elambda__1___closed__4;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_axiom;
|
||||
lean_object* l_Lean_Parser_Command_exit___closed__2;
|
||||
lean_object* l_Lean_Parser_Command_openOnly___closed__4;
|
||||
|
|
@ -1541,7 +1541,7 @@ lean_object* x_24; lean_object* x_25; uint8_t x_26;
|
|||
x_24 = lean_ctor_get(x_23, 1);
|
||||
lean_inc(x_24);
|
||||
lean_dec(x_23);
|
||||
x_25 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
x_25 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
x_26 = lean_string_dec_eq(x_24, x_25);
|
||||
lean_dec(x_24);
|
||||
if (x_26 == 0)
|
||||
|
|
@ -1796,7 +1796,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Term_stxQuot___closed__3;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__6;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__6;
|
||||
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -10269,7 +10269,7 @@ lean_object* x_67; lean_object* x_68; uint8_t x_69;
|
|||
x_67 = lean_ctor_get(x_66, 1);
|
||||
lean_inc(x_67);
|
||||
lean_dec(x_66);
|
||||
x_68 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1;
|
||||
x_68 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__1;
|
||||
x_69 = lean_string_dec_eq(x_67, x_68);
|
||||
lean_dec(x_67);
|
||||
if (x_69 == 0)
|
||||
|
|
@ -10370,7 +10370,7 @@ lean_object* x_38; lean_object* x_39; uint8_t x_40;
|
|||
x_38 = lean_ctor_get(x_37, 1);
|
||||
lean_inc(x_38);
|
||||
lean_dec(x_37);
|
||||
x_39 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
x_39 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
x_40 = lean_string_dec_eq(x_38, x_39);
|
||||
lean_dec(x_38);
|
||||
if (x_40 == 0)
|
||||
|
|
@ -10471,8 +10471,8 @@ lean_object* _init_l_Lean_Parser_Command_strictInferMod___closed__1() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__2;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__6;
|
||||
x_1 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__2;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__6;
|
||||
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -12137,7 +12137,7 @@ lean_object* x_107; lean_object* x_108; uint8_t x_109;
|
|||
x_107 = lean_ctor_get(x_106, 1);
|
||||
lean_inc(x_107);
|
||||
lean_dec(x_106);
|
||||
x_108 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1;
|
||||
x_108 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__1;
|
||||
x_109 = lean_string_dec_eq(x_107, x_108);
|
||||
lean_dec(x_107);
|
||||
if (x_109 == 0)
|
||||
|
|
@ -12202,7 +12202,7 @@ lean_object* x_26; lean_object* x_27; uint8_t x_28;
|
|||
x_26 = lean_ctor_get(x_25, 1);
|
||||
lean_inc(x_26);
|
||||
lean_dec(x_25);
|
||||
x_27 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
x_27 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
x_28 = lean_string_dec_eq(x_26, x_27);
|
||||
lean_dec(x_26);
|
||||
if (x_28 == 0)
|
||||
|
|
@ -12480,7 +12480,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Command_structExplicitBinder___closed__2;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__6;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__6;
|
||||
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -12521,7 +12521,7 @@ lean_object* _init_l_Lean_Parser_Command_structExplicitBinder___closed__7() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__2;
|
||||
x_1 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__2;
|
||||
x_2 = l_Lean_Parser_Command_structExplicitBinder___closed__6;
|
||||
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
|
||||
return x_3;
|
||||
|
|
@ -14963,7 +14963,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Command_extends___closed__1;
|
||||
x_2 = l_Lean_Parser_Term_matchAlt___closed__1;
|
||||
x_2 = l_Lean_Parser_Term_matchAlt___closed__3;
|
||||
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -22136,7 +22136,7 @@ lean_object* x_26; lean_object* x_27; uint8_t x_28;
|
|||
x_26 = lean_ctor_get(x_25, 1);
|
||||
lean_inc(x_26);
|
||||
lean_dec(x_25);
|
||||
x_27 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
x_27 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
x_28 = lean_string_dec_eq(x_26, x_27);
|
||||
lean_dec(x_26);
|
||||
if (x_28 == 0)
|
||||
|
|
@ -22290,7 +22290,7 @@ lean_object* x_76; lean_object* x_77; uint8_t x_78;
|
|||
x_76 = lean_ctor_get(x_75, 1);
|
||||
lean_inc(x_76);
|
||||
lean_dec(x_75);
|
||||
x_77 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1;
|
||||
x_77 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__1;
|
||||
x_78 = lean_string_dec_eq(x_76, x_77);
|
||||
lean_dec(x_76);
|
||||
if (x_78 == 0)
|
||||
|
|
@ -22377,7 +22377,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
|||
x_1 = l_Lean_Parser_Level_ident___elambda__1___closed__4;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
x_3 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__6;
|
||||
x_3 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__6;
|
||||
x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
|
|
@ -22386,7 +22386,7 @@ lean_object* _init_l_Lean_Parser_Command_export___closed__3() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__2;
|
||||
x_1 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__2;
|
||||
x_2 = l_Lean_Parser_Command_export___closed__2;
|
||||
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
|
||||
return x_3;
|
||||
|
|
@ -24084,7 +24084,7 @@ lean_object* x_83; lean_object* x_84; uint8_t x_85;
|
|||
x_83 = lean_ctor_get(x_82, 1);
|
||||
lean_inc(x_83);
|
||||
lean_dec(x_82);
|
||||
x_84 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1;
|
||||
x_84 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__1;
|
||||
x_85 = lean_string_dec_eq(x_83, x_84);
|
||||
lean_dec(x_83);
|
||||
if (x_85 == 0)
|
||||
|
|
@ -24201,7 +24201,7 @@ lean_object* x_27; lean_object* x_28; uint8_t x_29;
|
|||
x_27 = lean_ctor_get(x_26, 1);
|
||||
lean_inc(x_27);
|
||||
lean_dec(x_26);
|
||||
x_28 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
x_28 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
x_29 = lean_string_dec_eq(x_27, x_28);
|
||||
lean_dec(x_27);
|
||||
if (x_29 == 0)
|
||||
|
|
@ -24360,7 +24360,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
|||
x_1 = l_Lean_Parser_Level_ident___elambda__1___closed__4;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
x_3 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__2;
|
||||
x_3 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__2;
|
||||
x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -29,7 +29,6 @@ lean_object* l_Lean_Parser_Level_num___closed__4;
|
|||
lean_object* l_Lean_Parser_Level_max___elambda__1___closed__6;
|
||||
lean_object* l_Lean_Parser_regBuiltinLevelParserAttr(lean_object*);
|
||||
lean_object* l_Lean_Parser_Level_num___elambda__1___closed__4;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
lean_object* l_Lean_Parser_Level_hole___closed__5;
|
||||
lean_object* l_Lean_Parser_Level_hole___closed__3;
|
||||
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Level_max___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -107,6 +106,7 @@ lean_object* l_Lean_Parser_Level_ident___elambda__1___closed__4;
|
|||
lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Level_ident___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Level_paren___closed__4;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__6;
|
||||
lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Level_paren___closed__9;
|
||||
lean_object* l_Lean_Parser_Level_addLit___closed__7;
|
||||
|
|
@ -114,7 +114,6 @@ lean_object* l_Lean_Parser_categoryParserFn(lean_object*, lean_object*, lean_obj
|
|||
lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__6;
|
||||
lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__1;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
lean_object* l_Lean_Parser_Level_ident___closed__2;
|
||||
extern lean_object* l_Lean_Parser_appPrec;
|
||||
lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__3;
|
||||
|
|
@ -129,11 +128,11 @@ lean_object* l_Lean_Parser_Level_num;
|
|||
lean_object* l_Lean_Parser_categoryParser(uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Level_max___closed__5;
|
||||
lean_object* l_Lean_Parser_Level_num___closed__3;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__10;
|
||||
lean_object* l_Lean_Parser_symbolInfo(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_epsilonInfo;
|
||||
lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__6;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1;
|
||||
extern lean_object* l_Lean_mkHole___closed__1;
|
||||
lean_object* l_Lean_Parser_Level_ident___closed__4;
|
||||
lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__7;
|
||||
|
|
@ -142,7 +141,6 @@ lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__9;
|
|||
lean_object* l___regBuiltinParser_Lean_Parser_Level_hole(lean_object*);
|
||||
lean_object* l_Lean_Parser_Level_hole___closed__1;
|
||||
extern lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__3;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__6;
|
||||
lean_object* l_String_trim(lean_object*);
|
||||
lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__8;
|
||||
lean_object* l_Lean_Parser_Level_hole___closed__2;
|
||||
|
|
@ -159,12 +157,14 @@ lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__5;
|
|||
lean_object* l_Lean_Parser_Level_max___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Level_imax___closed__1;
|
||||
lean_object* l_Lean_Parser_Level_imax___closed__6;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__1;
|
||||
lean_object* l_Lean_Parser_Level_addLit___closed__4;
|
||||
lean_object* l_Lean_Parser_ParserState_mkUnexpectedError(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Level_paren___closed__6;
|
||||
lean_object* l___regBuiltinParser_Lean_Parser_Level_imax(lean_object*);
|
||||
lean_object* l_Lean_Parser_Level_imax___closed__4;
|
||||
lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__7;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
lean_object* l_Lean_Parser_Level_paren___closed__8;
|
||||
lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__4;
|
||||
lean_object* l_Lean_Parser_Level_hole___closed__4;
|
||||
|
|
@ -265,7 +265,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Level_paren___elambda__1___closed__2;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -285,7 +285,7 @@ _start:
|
|||
{
|
||||
uint8_t x_1; lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
|
||||
x_1 = 0;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
x_3 = l_Lean_Parser_Level_paren___elambda__1___closed__4;
|
||||
x_4 = 1;
|
||||
x_5 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3, x_4);
|
||||
|
|
@ -297,7 +297,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Char_HasRepr___closed__1;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
x_3 = lean_string_append(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -329,7 +329,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Char_HasRepr___closed__1;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__1;
|
||||
x_3 = lean_string_append(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -425,7 +425,7 @@ lean_object* x_60; lean_object* x_61; uint8_t x_62;
|
|||
x_60 = lean_ctor_get(x_59, 1);
|
||||
lean_inc(x_60);
|
||||
lean_dec(x_59);
|
||||
x_61 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1;
|
||||
x_61 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__1;
|
||||
x_62 = lean_string_dec_eq(x_60, x_61);
|
||||
lean_dec(x_60);
|
||||
if (x_62 == 0)
|
||||
|
|
@ -499,7 +499,7 @@ lean_object* x_28; lean_object* x_29; uint8_t x_30;
|
|||
x_28 = lean_ctor_get(x_27, 1);
|
||||
lean_inc(x_28);
|
||||
lean_dec(x_27);
|
||||
x_29 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
x_29 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
x_30 = lean_string_dec_eq(x_28, x_29);
|
||||
lean_dec(x_28);
|
||||
if (x_30 == 0)
|
||||
|
|
@ -592,7 +592,7 @@ lean_object* _init_l_Lean_Parser_Level_paren___closed__2() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1;
|
||||
x_1 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__1;
|
||||
x_2 = l_Lean_Parser_Level_paren___closed__1;
|
||||
x_3 = l_Lean_Parser_symbolInfo(x_1, x_2);
|
||||
return x_3;
|
||||
|
|
@ -616,7 +616,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
|||
x_1 = l_Lean_Parser_Level_paren___closed__3;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
x_3 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__6;
|
||||
x_3 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__6;
|
||||
x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -65,7 +65,6 @@ lean_object* l_Lean_Parser_Command_macroTailDefault___closed__8;
|
|||
lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__7;
|
||||
lean_object* l_Lean_Parser_regBuiltinSyntaxParserAttr___closed__2;
|
||||
lean_object* l_Lean_Parser_Command_infixr___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
extern lean_object* l_Lean_Parser_regBuiltinCommandParserAttr___closed__4;
|
||||
lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__5;
|
||||
lean_object* l_Lean_Parser_Command_quotedSymbolPrec___closed__5;
|
||||
|
|
@ -384,6 +383,7 @@ lean_object* l_Lean_Parser_Command_notation___elambda__1___closed__6;
|
|||
lean_object* l_Lean_Parser_Command_reserve;
|
||||
lean_object* l_Lean_Parser_Syntax_sepBy___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_mixfixKind;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__2;
|
||||
lean_object* l_Lean_Parser_Syntax_ident___closed__2;
|
||||
lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Command_macroTailDefault___closed__6;
|
||||
|
|
@ -399,6 +399,7 @@ lean_object* l_Lean_Parser_Syntax_atom___closed__4;
|
|||
lean_object* l___regBuiltinParser_Lean_Parser_Syntax_sepBy(lean_object*);
|
||||
lean_object* l_Lean_Parser_Syntax_atom;
|
||||
lean_object* l_Lean_Parser_Syntax_sepBy___elambda__1___closed__8;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__6;
|
||||
extern lean_object* l_Lean_Parser_mkAntiquot___closed__7;
|
||||
lean_object* l_Lean_Parser_Command_macroTailCommand___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_identPrec___closed__4;
|
||||
|
|
@ -422,7 +423,6 @@ lean_object* l_Lean_Parser_precedence;
|
|||
lean_object* l_Lean_Parser_quotedSymbolFn___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Syntax_sepBy1___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_precedenceLit___closed__3;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
lean_object* l_Lean_Parser_Syntax_optional;
|
||||
lean_object* l_Lean_Parser_Syntax_atom___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_macroTailTactic___closed__4;
|
||||
|
|
@ -467,7 +467,6 @@ lean_object* l_Lean_Parser_mergeOrElseErrors(lean_object*, lean_object*, lean_ob
|
|||
lean_object* l_Lean_Parser_Syntax_cat___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Command_reserve___closed__6;
|
||||
lean_object* l_Lean_Parser_Syntax_sepBy1___closed__1;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__2;
|
||||
extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__9;
|
||||
extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__8;
|
||||
lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__4;
|
||||
|
|
@ -492,6 +491,7 @@ lean_object* l_Lean_Parser_Command_macroTailTactic___closed__6;
|
|||
lean_object* l_Lean_Parser_Command_notation___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_macroTailCommand___closed__4;
|
||||
lean_object* l_Lean_Parser_Command_infixl___elambda__1___closed__7;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
lean_object* l_Lean_Parser_Syntax_lookahead___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__8;
|
||||
lean_object* l_Lean_Parser_symbolInfo(lean_object*, lean_object*);
|
||||
|
|
@ -504,7 +504,6 @@ extern lean_object* l_Lean_Parser_epsilonInfo;
|
|||
lean_object* l_Lean_Parser_Command_macroTailDefault;
|
||||
lean_object* l_Lean_Parser_Command_mixfix___closed__6;
|
||||
lean_object* l_Lean_Parser_unquotedSymbol(uint8_t);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_macro___elambda__1___closed__7;
|
||||
lean_object* l_Lean_Parser_Syntax_ident___closed__1;
|
||||
extern lean_object* l_Lean_Parser_Term_typeAscription___closed__1;
|
||||
|
|
@ -544,7 +543,6 @@ lean_object* l_Lean_Parser_Command_notation___elambda__1___closed__3;
|
|||
lean_object* l_Lean_Parser_Command_mixfixKind___closed__6;
|
||||
lean_object* l_Lean_Parser_Command_macro___elambda__1___closed__8;
|
||||
extern lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__3;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__6;
|
||||
lean_object* l_Lean_Parser_Syntax_orelse___closed__2;
|
||||
lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__4;
|
||||
lean_object* l_Lean_Parser_Syntax_char___closed__3;
|
||||
|
|
@ -611,6 +609,7 @@ lean_object* l_Lean_Parser_precedence___closed__2;
|
|||
lean_object* l_Lean_Parser_Syntax_char___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Parser_regBuiltinTacticParserAttr___closed__4;
|
||||
lean_object* l_Lean_Parser_Command_infixr___closed__4;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__1;
|
||||
lean_object* l_Lean_Parser_Syntax_try___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Command_macroTailDefault___closed__4;
|
||||
lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__6;
|
||||
|
|
@ -649,6 +648,7 @@ lean_object* l_Lean_Parser_maxPrec___closed__1;
|
|||
lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__1;
|
||||
lean_object* l___regBuiltinParser_Lean_Parser_Command_syntax(lean_object*);
|
||||
lean_object* l_Lean_Parser_Syntax_atom___closed__3;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
lean_object* l_Lean_Parser_Command_quotedSymbolPrec___closed__6;
|
||||
lean_object* l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__5;
|
||||
extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__1;
|
||||
|
|
@ -1549,7 +1549,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Syntax_paren___elambda__1___closed__2;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -1569,7 +1569,7 @@ _start:
|
|||
{
|
||||
uint8_t x_1; lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
|
||||
x_1 = 0;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
x_3 = l_Lean_Parser_Syntax_paren___elambda__1___closed__4;
|
||||
x_4 = 1;
|
||||
x_5 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3, x_4);
|
||||
|
|
@ -1648,7 +1648,7 @@ lean_object* x_71; lean_object* x_72; uint8_t x_73;
|
|||
x_71 = lean_ctor_get(x_70, 1);
|
||||
lean_inc(x_71);
|
||||
lean_dec(x_70);
|
||||
x_72 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1;
|
||||
x_72 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__1;
|
||||
x_73 = lean_string_dec_eq(x_71, x_72);
|
||||
lean_dec(x_71);
|
||||
if (x_73 == 0)
|
||||
|
|
@ -1713,7 +1713,7 @@ lean_object* x_24; lean_object* x_25; uint8_t x_26;
|
|||
x_24 = lean_ctor_get(x_23, 1);
|
||||
lean_inc(x_24);
|
||||
lean_dec(x_23);
|
||||
x_25 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
x_25 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
x_26 = lean_string_dec_eq(x_24, x_25);
|
||||
lean_dec(x_24);
|
||||
if (x_26 == 0)
|
||||
|
|
@ -1852,7 +1852,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
|||
x_1 = l_Lean_Parser_Syntax_paren___closed__1;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
x_3 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__6;
|
||||
x_3 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__6;
|
||||
x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
|
|
@ -1861,7 +1861,7 @@ lean_object* _init_l_Lean_Parser_Syntax_paren___closed__3() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__2;
|
||||
x_1 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__2;
|
||||
x_2 = l_Lean_Parser_Syntax_paren___closed__2;
|
||||
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
|
||||
return x_3;
|
||||
|
|
@ -11277,7 +11277,7 @@ lean_object* x_15; lean_object* x_16; uint8_t x_17;
|
|||
x_15 = lean_ctor_get(x_14, 1);
|
||||
lean_inc(x_15);
|
||||
lean_dec(x_14);
|
||||
x_16 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
x_16 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
x_17 = lean_string_dec_eq(x_15, x_16);
|
||||
lean_dec(x_15);
|
||||
if (x_17 == 0)
|
||||
|
|
@ -11706,7 +11706,7 @@ lean_object* x_11; lean_object* x_12; uint8_t x_13;
|
|||
x_11 = lean_ctor_get(x_10, 1);
|
||||
lean_inc(x_11);
|
||||
lean_dec(x_10);
|
||||
x_12 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
x_12 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
x_13 = lean_string_dec_eq(x_11, x_12);
|
||||
lean_dec(x_11);
|
||||
if (x_13 == 0)
|
||||
|
|
@ -12038,7 +12038,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
|||
x_1 = l_Lean_Parser_Term_stxQuot___closed__2;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
x_3 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__6;
|
||||
x_3 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__6;
|
||||
x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
|
|
@ -12339,7 +12339,7 @@ lean_object* x_35; lean_object* x_36; uint8_t x_37;
|
|||
x_35 = lean_ctor_get(x_34, 1);
|
||||
lean_inc(x_35);
|
||||
lean_dec(x_34);
|
||||
x_36 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
x_36 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
x_37 = lean_string_dec_eq(x_35, x_36);
|
||||
lean_dec(x_35);
|
||||
if (x_37 == 0)
|
||||
|
|
@ -12551,7 +12551,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
|||
x_1 = l_Lean_Parser_Command_macroTailDefault___closed__2;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
x_3 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__6;
|
||||
x_3 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__6;
|
||||
x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -50,7 +50,6 @@ extern lean_object* l_Lean_Parser_Term_have___elambda__1___closed__10;
|
|||
lean_object* l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Term_tacticStxQuot___elambda__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_seq;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
lean_object* l_Lean_Parser_Tactic_skip___closed__3;
|
||||
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Tactic_seq___elambda__1___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_traceState___elambda__1___closed__5;
|
||||
|
|
@ -235,6 +234,7 @@ lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1(lean_object*, l
|
|||
extern lean_object* l_Lean_Parser_Level_ident___elambda__1___closed__4;
|
||||
lean_object* l_Lean_Parser_Tactic_apply;
|
||||
lean_object* l_Lean_Parser_Tactic_assumption___closed__5;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__2;
|
||||
lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_paren___closed__1;
|
||||
lean_object* l_Lean_Parser_Term_tacticStxQuot___elambda__1___closed__7;
|
||||
|
|
@ -242,6 +242,7 @@ lean_object* l_Lean_Parser_Tactic_paren___closed__2;
|
|||
lean_object* l_Lean_Parser_ParserState_popSyntax(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_paren___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__1;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__6;
|
||||
lean_object* l___regBuiltinParser_Lean_Parser_Term_tacticStxQuot___closed__1;
|
||||
extern lean_object* l_Lean_Parser_Term_seq___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__1;
|
||||
|
|
@ -255,7 +256,6 @@ lean_object* l_Lean_Parser_categoryParserFn(lean_object*, lean_object*, lean_obj
|
|||
lean_object* l_Lean_Parser_Tactic_intros___closed__4;
|
||||
lean_object* l___regBuiltinParser_Lean_Parser_Term_tacticStxQuot___closed__2;
|
||||
lean_object* l_Lean_Parser_sepBy1Info(lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__5;
|
||||
lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__6;
|
||||
lean_object* l_Lean_Parser_Tactic_underscoreFn(uint8_t, lean_object*);
|
||||
|
|
@ -271,7 +271,6 @@ lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__1;
|
|||
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_allGoals(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_underscoreFn___rarg___closed__3;
|
||||
lean_object* l_Lean_Parser_mergeOrElseErrors(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_refine___closed__4;
|
||||
lean_object* l_Lean_Parser_categoryParser(uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_exact;
|
||||
|
|
@ -281,6 +280,7 @@ lean_object* l_Lean_Parser_regTacticParserAttribute(lean_object*);
|
|||
lean_object* l_Lean_Parser_Tactic_allGoals___closed__5;
|
||||
lean_object* l_Lean_Parser_Tactic_paren___closed__6;
|
||||
lean_object* l_Lean_Parser_Tactic_skip___elambda__1___closed__4;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
lean_object* l_Lean_Parser_symbolInfo(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_underscoreFn___rarg___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_apply___elambda__1___closed__6;
|
||||
|
|
@ -289,7 +289,6 @@ lean_object* l_Lean_Parser_Tactic_orelse___elambda__1___closed__1;
|
|||
lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___closed__4;
|
||||
lean_object* l_Lean_Parser_Tactic_assumption___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_case___elambda__1___closed__7;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1;
|
||||
extern lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__11;
|
||||
lean_object* l_Lean_Parser_Term_tacticBlock___closed__4;
|
||||
lean_object* l_Lean_Parser_Term_tacticBlock___closed__1;
|
||||
|
|
@ -307,7 +306,6 @@ lean_object* l_Lean_Parser_Tactic_intros;
|
|||
lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Tactic_nestedTacticBlockCurly___closed__5;
|
||||
lean_object* l_Lean_Parser_Tactic_case___closed__7;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__6;
|
||||
lean_object* l_Lean_Parser_Term_tacticStxQuot___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_exact___closed__4;
|
||||
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_paren(lean_object*);
|
||||
|
|
@ -343,6 +341,7 @@ lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__2;
|
|||
lean_object* l_Lean_Parser_Term_tacticBlock___elambda__1___closed__4;
|
||||
lean_object* l_Lean_Parser_Tactic_orelse___closed__6;
|
||||
lean_object* l_Lean_Parser_Tactic_intro___closed__5;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_exact___elambda__1___closed__7;
|
||||
lean_object* l___regBuiltinParser_Lean_Parser_Tactic_skip(lean_object*);
|
||||
lean_object* l_Lean_Parser_Tactic_intros___elambda__1___closed__4;
|
||||
|
|
@ -370,6 +369,7 @@ lean_object* l_Lean_Parser_Tactic_paren;
|
|||
lean_object* l_Lean_Parser_Tactic_nestedTacticBlock___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_intro;
|
||||
lean_object* l_Lean_Parser_tacticParser___boxed(lean_object*, lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_refine;
|
||||
extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_Tactic_seq___elambda__1(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -3675,7 +3675,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Tactic_seq___elambda__1___closed__2;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -3695,7 +3695,7 @@ _start:
|
|||
{
|
||||
uint8_t x_1; lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
|
||||
x_1 = 0;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__1;
|
||||
x_3 = l_Lean_Parser_Tactic_paren___elambda__1___closed__2;
|
||||
x_4 = 1;
|
||||
x_5 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3, x_4);
|
||||
|
|
@ -3774,7 +3774,7 @@ lean_object* x_58; lean_object* x_59; uint8_t x_60;
|
|||
x_58 = lean_ctor_get(x_57, 1);
|
||||
lean_inc(x_58);
|
||||
lean_dec(x_57);
|
||||
x_59 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__1;
|
||||
x_59 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__1;
|
||||
x_60 = lean_string_dec_eq(x_58, x_59);
|
||||
lean_dec(x_58);
|
||||
if (x_60 == 0)
|
||||
|
|
@ -3847,7 +3847,7 @@ lean_object* x_26; lean_object* x_27; uint8_t x_28;
|
|||
x_26 = lean_ctor_get(x_25, 1);
|
||||
lean_inc(x_26);
|
||||
lean_dec(x_25);
|
||||
x_27 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
x_27 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
x_28 = lean_string_dec_eq(x_26, x_27);
|
||||
lean_dec(x_26);
|
||||
if (x_28 == 0)
|
||||
|
|
@ -3934,7 +3934,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
|||
x_1 = l_Lean_Parser_Tactic_nonEmptySeq;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_2);
|
||||
x_3 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__6;
|
||||
x_3 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__6;
|
||||
x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
|
||||
return x_4;
|
||||
}
|
||||
|
|
@ -3943,7 +3943,7 @@ lean_object* _init_l_Lean_Parser_Tactic_paren___closed__2() {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__2;
|
||||
x_1 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__2;
|
||||
x_2 = l_Lean_Parser_Tactic_paren___closed__1;
|
||||
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
|
||||
return x_3;
|
||||
|
|
@ -5580,7 +5580,7 @@ lean_object* x_17; lean_object* x_18; uint8_t x_19;
|
|||
x_17 = lean_ctor_get(x_16, 1);
|
||||
lean_inc(x_17);
|
||||
lean_dec(x_16);
|
||||
x_18 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__5;
|
||||
x_18 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__5;
|
||||
x_19 = lean_string_dec_eq(x_17, x_18);
|
||||
lean_dec(x_17);
|
||||
if (x_19 == 0)
|
||||
|
|
@ -5660,7 +5660,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_Tactic_seq___closed__2;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___closed__6;
|
||||
x_2 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___closed__6;
|
||||
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -32,7 +32,6 @@ lean_object* l_Lean_SourceInfo_truncateTrailing(lean_object*);
|
|||
lean_object* l_Array_back___at___private_Init_Lean_Parser_Parser_6__nameLitAux___spec__1(lean_object*);
|
||||
lean_object* l_Lean_Syntax_manyToSepBy(lean_object*, lean_object*);
|
||||
extern lean_object* l_Array_forMAux___main___at_Lean_Environment_displayStats___spec__9___closed__2;
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
extern lean_object* l_Option_HasRepr___rarg___closed__3;
|
||||
extern lean_object* l_Lean_Syntax_inhabited;
|
||||
lean_object* l_Lean_Syntax_getNumArgs(lean_object*);
|
||||
|
|
@ -42,6 +41,7 @@ lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_manyToSepBy___spec__1__
|
|||
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_mkOptionalNode___closed__2;
|
||||
lean_object* l_Lean_Syntax_getTailInfo___main(lean_object*);
|
||||
extern lean_object* l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
|
||||
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_manyToSepBy___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
|
|
@ -210,7 +210,7 @@ if (lean_obj_tag(x_1) == 1)
|
|||
lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5;
|
||||
x_2 = lean_ctor_get(x_1, 0);
|
||||
x_3 = lean_ctor_get(x_1, 1);
|
||||
x_4 = l___private_Init_Lean_Parser_Parser_14__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_4 = l___private_Init_Lean_Parser_Parser_13__antiquotNestedExpr___elambda__1___rarg___closed__2;
|
||||
x_5 = lean_name_eq(x_2, x_4);
|
||||
if (x_5 == 0)
|
||||
{
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue