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

chore: update-stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-12 08:28:40 -08:00
parent 554d0b4d4c
commit bb8cd95437
20 changed files with 10643 additions and 8216 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Init/Data/Array/Basic.lean generated
View file

@ -486,7 +486,7 @@ export Array (mkArray)
syntax "#[" sepBy(term, ", ") "]" : term
macro_rules
| `(#[ $elems* ]) => `(List.toArray [ $elems* ])
| `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
namespace Array

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

@ -121,16 +121,16 @@ syntax "%[" term,* "|" term "]" : term -- auxiliary notation for creating big li
namespace Lean
macro_rules
| `([ $elems* ]) => do
| `([ $elems,* ]) => do
let rec expandListLit (i : Nat) (skip : Bool) (result : Syntax) : MacroM Syntax := do
match i, skip with
| 0, _ => pure result
| i+1, true => expandListLit i false result
| i+1, false => expandListLit i true (← `(List.cons $(elems[i]) $result))
if elems.size < 64 then
expandListLit elems.size false (← `(List.nil))
| i+1, false => expandListLit i true (← `(List.cons $(elems.elemsAndSeps[i]) $result))
if elems.elemsAndSeps.size < 64 then
expandListLit elems.elemsAndSeps.size false (← `(List.nil))
else
`(%[ $elems* | List.nil ])
`(%[ $elems,* | List.nil ])
namespace Parser.Tactic

19
stage0/src/Lean/Elab/App.lean generated
View file

@ -384,7 +384,8 @@ private def processExplictArg (k : M Expr) : M Expr := do
match evalSyntaxConstant env opts tacticDecl with
| Except.error err => throwError err
| Except.ok tacticSyntax =>
let tacticBlock ← `(by { $(tacticSyntax.getArgs)* })
-- TODO(Leo): does this work correctly for tactic sequences?
let tacticBlock ← `(by $tacticSyntax)
-- tacticBlock does not have any position information.
-- So, we use the current ref
let ref ← getRef
@ -800,12 +801,12 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
throwError "unexpected occurrence of named pattern"
| `($id:ident) => do
elabAppFnId id [] lvals namedArgs args expectedType? explicit ellipsis overloaded acc
| `($id:ident.{$us*}) => do
let us ← elabExplicitUnivs us.getSepElems
| `($id:ident.{$us,*}) => do
let us ← elabExplicitUnivs us
elabAppFnId id us lvals namedArgs args expectedType? explicit ellipsis overloaded acc
| `(@$id:ident) =>
elabAppFn id lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
| `(@$id:ident.{$us*}) =>
| `(@$id:ident.{$us,*}) =>
elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
| `(@$t) => throwUnsupportedSyntax -- invalid occurrence of `@`
| `(_) => throwError "placeholders '_' cannot be used where a function is expected"
@ -916,11 +917,11 @@ private def elabAtom : TermElab := fun stx expectedType? =>
@[builtinTermElab explicit] def elabExplicit : TermElab := fun stx expectedType? =>
match stx with
| `(@$id:ident) => elabAtom stx expectedType? -- Recall that `elabApp` also has support for `@`
| `(@$id:ident.{$us*}) => elabAtom stx expectedType?
| `(@($t)) => elabTermWithoutImplicitLambdas t expectedType? -- `@` is being used just to disable implicit lambdas
| `(@$t) => elabTermWithoutImplicitLambdas t expectedType? -- `@` is being used just to disable implicit lambdas
| _ => throwUnsupportedSyntax
| `(@$id:ident) => elabAtom stx expectedType? -- Recall that `elabApp` also has support for `@`
| `(@$id:ident.{$us,*}) => elabAtom stx expectedType?
| `(@($t)) => elabTermWithoutImplicitLambdas t expectedType? -- `@` is being used just to disable implicit lambdas
| `(@$t) => elabTermWithoutImplicitLambdas t expectedType? -- `@` is being used just to disable implicit lambdas
| _ => throwUnsupportedSyntax
@[builtinTermElab choice] def elabChoice : TermElab := elabAtom
@[builtinTermElab proj] def elabProj : TermElab := elabAtom

8
stage0/src/Lean/Elab/BuiltinNotation.lean generated
View file

@ -14,7 +14,7 @@ open Meta
@[builtinTermElab anonymousCtor] def elabAnonymousCtor : TermElab := fun stx expectedType? =>
match stx with
| `(⟨$args*⟩) => do
| `(⟨$args,*⟩) => do
tryPostponeIfNoneOrMVar expectedType?
match expectedType? with
| some expectedType =>
@ -24,7 +24,7 @@ open Meta
(fun ival us => do
match ival.ctors with
| [ctor] =>
let newStx ← `($(mkCIdentFrom stx ctor) $(args.getSepElems)*)
let newStx ← `($(mkCIdentFrom stx ctor) $(args)*)
withMacroExpansion stx newStx $ elabTerm newStx expectedType?
| _ => throwError! "invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor {indentExpr expectedType}")
| none => throwError "invalid constructor ⟨...⟩, expected type must be known"
@ -262,8 +262,8 @@ private def elabCDot (stx : Syntax) (expectedType? : Option Expr) : TermElabM Ex
let e ← elabCDot e type
ensureHasType type e
| `(($e)) => elabCDot e expectedType?
| `(($e, $es*)) => do
let pairs ← liftMacroM $ mkPairs (#[e] ++ es.getEvenElems)
| `(($e, $es,*)) => do
let pairs ← liftMacroM $ mkPairs (#[e] ++ es)
withMacroExpansion stx pairs (elabTerm pairs expectedType?)
| _ => throwError "unexpected parentheses notation"

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

@ -352,7 +352,7 @@ def elabMacroRulesAux (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM
else
throwErrorAt! alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
`(@[macro $(Lean.mkIdent k)] def myMacro : Macro :=
fun | $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
fun | $(SepArray.mk alts):matchAlt|* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
def inferMacroRulesAltKind (alt : Syntax) : CommandElabM SyntaxNodeKind := do
let lhs := alt[0]
@ -374,13 +374,13 @@ def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
if altsNotK.isEmpty then
pure defCmd
else
`($defCmd:command macro_rules $altsNotK:matchAlt*)
`($defCmd:command macro_rules $(SepArray.mk altsNotK):matchAlt|*)
@[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
adaptExpander fun stx => match stx with
| `(macro_rules $[|]? $alts:matchAlt*) => elabNoKindMacroRulesAux alts
| `(macro_rules [$kind] $[|]? $alts:matchAlt*) => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts
| _ => throwUnsupportedSyntax
| `(macro_rules $[|]? $alts:matchAlt|*) => elabNoKindMacroRulesAux alts.elemsAndSeps
| `(macro_rules [$kind] $[|]? $alts:matchAlt|*) => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts.elemsAndSeps
| _ => throwUnsupportedSyntax
-- TODO: cleanup after we have support for optional syntax at `match_syntax`
@[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro := fun stx =>
@ -478,9 +478,9 @@ private def expandNotationAux (ref : Syntax)
let fullKind := currNamespace ++ kind
let pat := Syntax.node fullKind patArgs
let stxDecl ← match attrKind with
| AttributeKind.global => `(syntax $[: $prec?]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
| AttributeKind.scoped => `(scoped syntax $[: $prec? ]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
| AttributeKind.local => `(local syntax $[: $prec? ]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
| AttributeKind.global => `(syntax $[: $prec?]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $[$syntaxParts]* : $cat)
| AttributeKind.scoped => `(scoped syntax $[: $prec? ]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $[$syntaxParts]* : $cat)
| AttributeKind.local => `(local syntax $[: $prec? ]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $[$syntaxParts]* : $cat)
let macroDecl ← `(macro_rules | `($pat) => `($qrhs))
match (← mkSimpleDelab vars pat qrhs |>.run) with
| some delabDecl => mkNullNode #[stxDecl, macroDecl, delabDecl]
@ -523,7 +523,7 @@ def expandOptPrio (stx : Syntax) : Nat :=
stx[1].isNatLit?.getD 0
def expandMacro (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
let prec := stx[1].getArgs
let prec := stx[1].getOptional?
let prio := expandOptPrio stx[2]
let head := stx[3]
let args := stx[4].getArgs
@ -543,12 +543,13 @@ def expandMacro (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := d
if stx.getArgs.size == 9 then
-- `stx` is of the form `macro $head $args* : $cat => term`
let rhs := stx[8]
`(syntax $prec* [$(mkIdentFrom stx kind):ident, $(quote prio):numLit] $stxParts* : $cat
-- NOTE: can't use `$stxParts*` here because it would interpret as a single antiquotation with the `stx` star postfix operator
`(syntax $(prec)? [$(mkIdentFrom stx kind):ident, $(quote prio):numLit] $[$stxParts]* : $cat
macro_rules | `($pat) => $rhs)
else
-- `stx` is of the form `macro $head $args* : $cat => `( $body )`
let rhsBody := stx[9]
`(syntax $prec* [$(mkIdentFrom stx kind):ident, $(quote prio):numLit] $stxParts* : $cat
`(syntax $(prec)? [$(mkIdentFrom stx kind):ident, $(quote prio):numLit] $[$stxParts]* : $cat
macro_rules | `($pat) => `($rhsBody))
@[builtinCommandElab «macro»] def elabMacro : CommandElab :=
@ -570,7 +571,7 @@ parser! "elab " >> optPrecedence >> optPrio >> elabHead >> many elabArg >> elabT
-/
def expandElab (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
let ref := stx
let prec := stx[1].getArgs
let prec := stx[1].getOptional?
let prio := expandOptPrio stx[2]
let head := stx[3]
let args := stx[4].getArgs
@ -592,7 +593,7 @@ def expandElab (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
if expectedTypeSpec.hasArgs then
if catName == `term then
let expId := expectedTypeSpec[1]
`(syntax $prec* [$kindId:ident, $(quote prio):numLit] $stxParts* : $cat
`(syntax $(prec)? [$kindId:ident, $(quote prio):numLit] $[$stxParts]* : $cat
@[termElab $kindId:ident] def elabFn : Lean.Elab.Term.TermElab :=
fun stx expectedType? => match stx with
| `($pat) => Lean.Elab.Command.withExpectedType expectedType? fun $expId => $rhs
@ -600,19 +601,19 @@ def expandElab (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
else
throwErrorAt! expectedTypeSpec "syntax category '{catName}' does not support expected type specification"
else if catName == `term then
`(syntax $prec* [$kindId:ident, $(quote prio):numLit] $stxParts* : $cat
`(syntax $(prec)? [$kindId:ident, $(quote prio):numLit] $[$stxParts]* : $cat
@[termElab $kindId:ident] def elabFn : Lean.Elab.Term.TermElab :=
fun stx _ => match stx with
| `($pat) => $rhs
| _ => throwUnsupportedSyntax)
else if catName == `command then
`(syntax $prec* [$kindId:ident, $(quote prio):numLit] $stxParts* : $cat
`(syntax $(prec)? [$kindId:ident, $(quote prio):numLit] $[$stxParts]* : $cat
@[commandElab $kindId:ident] def elabFn : Lean.Elab.Command.CommandElab :=
fun
| `($pat) => $rhs
| _ => throwUnsupportedSyntax)
else if catName == `tactic then
`(syntax $prec* [$kindId:ident, $(quote prio):numLit] $stxParts* : $cat
`(syntax $(prec)? [$kindId:ident, $(quote prio):numLit] $[$stxParts]* : $cat
@[tactic $kindId:ident] def elabFn : Lean.Elab.Tactic.Tactic :=
fun
| `(tactic|$pat) => $rhs

12
stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean generated
View file

@ -459,8 +459,8 @@ def delabTuple : Delab := whenPPOption getPPNotation do
let a ← withAppFn $ withAppArg delab
let b ← withAppArg delab
match b with
| `(($b, $bs*)) => `(($a, $b, $bs*))
| _ => `(($a, $b))
| `(($b, $bs,*)) => `(($a, $b, $bs,*))
| _ => `(($a, $b))
-- abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β
@[builtinDelab app.coe]
@ -488,15 +488,15 @@ def delabConsList : Delab := whenPPOption getPPNotation do
guard $ (← getExpr).getAppNumArgs == 3
let x ← withAppFn (withAppArg delab)
match (← withAppArg delab) with
| `([]) => `([$x])
| `([$xs*]) => `([$x, $xs*])
| _ => failure
| `([]) => `([$x])
| `([$xs,*]) => `([$x, $xs,*])
| _ => failure
@[builtinDelab app.List.toArray]
def delabListToArray : Delab := whenPPOption getPPNotation do
guard $ (← getExpr).getAppNumArgs == 2
match (← withAppArg delab) with
| `([$xs*]) => `(#[$xs*])
| `([$xs,*]) => `(#[$xs,*])
| _ => failure
@[builtinDelab app.namedPattern]

2
stage0/stdlib/CMakeLists.txt generated
View file

File diff suppressed because one or more lines are too long

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

File diff suppressed because it is too large Load diff

16
stage0/stdlib/Init/NotationExtra.c generated
View file

@ -210,7 +210,6 @@ extern lean_object* l_Lean_instInhabitedSyntax;
lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__50;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_1625____closed__2;
lean_object* l_Lean_unifConstraintElem___closed__5;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__5;
lean_object* l_Lean_mkSepArray(lean_object*, lean_object*);
lean_object* l_Lean_command__Unif__hint______Where___x7c_x2d_u22a2_____closed__19;
lean_object* l_term_u2203___x2c_____closed__5;
@ -273,12 +272,14 @@ lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2962__match__1___rarg(lea
lean_object* l_term_u03a3___x2c_____closed__4;
lean_object* l_Array_appendCore___rarg(lean_object*, lean_object*);
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2229____boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__5;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_49____closed__4;
lean_object* l_term___xd7_x27_____closed__1;
lean_object* l_term_u03a3___x2c_____closed__7;
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2318____closed__1;
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2962____closed__1;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_1625____closed__4;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__25;
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2318____closed__2;
lean_object* l_Array_ofSubarray___rarg(lean_object*);
@ -320,7 +321,6 @@ lean_object* l_Lean_expandExplicitBindersAux_loop___boxed(lean_object*, lean_obj
extern lean_object* l_Lean_myMacro____x40_Init_Notation___hyg_12778____closed__2;
lean_object* l_Array_mapMUnsafe_map___at_myMacro____x40_Init_NotationExtra___hyg_2962____spec__3___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__3;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__15;
lean_object* l_Lean_expandExplicitBindersAux_loop___closed__8;
lean_object* l_Lean_binderIdent___closed__2;
@ -2784,7 +2784,7 @@ x_233 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_233, 0, x_232);
lean_ctor_set(x_233, 1, x_231);
x_234 = lean_array_push(x_226, x_233);
x_235 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__5;
x_235 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__5;
x_236 = lean_array_push(x_235, x_182);
x_237 = lean_array_push(x_236, x_194);
x_238 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__46;
@ -2894,7 +2894,7 @@ x_298 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_298, 0, x_297);
lean_ctor_set(x_298, 1, x_296);
x_299 = lean_array_push(x_291, x_298);
x_300 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__5;
x_300 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__5;
x_301 = lean_array_push(x_300, x_246);
x_302 = lean_array_push(x_301, x_259);
x_303 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__46;
@ -3074,7 +3074,7 @@ x_89 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_89, 0, x_88);
lean_ctor_set(x_89, 1, x_87);
x_90 = lean_array_push(x_82, x_89);
x_91 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__5;
x_91 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__5;
x_92 = lean_array_push(x_91, x_42);
x_93 = lean_array_push(x_92, x_54);
x_94 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__46;
@ -3174,7 +3174,7 @@ x_150 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_150, 0, x_149);
lean_ctor_set(x_150, 1, x_148);
x_151 = lean_array_push(x_143, x_150);
x_152 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__5;
x_152 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__5;
x_153 = lean_array_push(x_152, x_102);
x_154 = lean_array_push(x_153, x_115);
x_155 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__46;
@ -4383,7 +4383,7 @@ x_50 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_50, 0, x_33);
lean_ctor_set(x_50, 1, x_49);
x_51 = lean_array_push(x_25, x_50);
x_52 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
x_52 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
x_53 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_53, 0, x_52);
lean_ctor_set(x_53, 1, x_51);
@ -4440,7 +4440,7 @@ x_82 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_82, 0, x_75);
lean_ctor_set(x_82, 1, x_81);
x_83 = lean_array_push(x_67, x_82);
x_84 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
x_84 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
x_85 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_85, 0, x_84);
lean_ctor_set(x_85, 1, x_83);

6682
stage0/stdlib/Lean/Elab/App.c generated
View file

File diff suppressed because it is too large Load diff

8
stage0/stdlib/Lean/Elab/Binders.c generated
View file

@ -409,6 +409,7 @@ lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__12;
lean_object* l_Lean_Elab_Term_quoteAutoTactic_match__1(lean_object*);
lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__1___closed__2;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_1625____closed__4;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_expandFunBinders_loop___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkExplicitBinder(lean_object*, lean_object*);
extern lean_object* l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_checkTypesAndAssign___closed__8;
@ -464,7 +465,6 @@ lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_elabForall__
lean_object* l_Lean_Elab_Term_quoteAutoTactic___closed__17;
lean_object* l_Lean_Elab_Term_elabLetDeclAux___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkLetRec(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
lean_object* l_Lean_setEnv___at_Lean_Elab_Term_declareTacticSyntax___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_expandExplicitBindersAux_loop___closed__8;
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
@ -17805,7 +17805,7 @@ x_79 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_79, 0, x_69);
lean_ctor_set(x_79, 1, x_78);
x_80 = lean_array_push(x_67, x_79);
x_81 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
x_81 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
x_82 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_82, 0, x_81);
lean_ctor_set(x_82, 1, x_80);
@ -17840,7 +17840,7 @@ x_97 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_97, 0, x_87);
lean_ctor_set(x_97, 1, x_96);
x_98 = lean_array_push(x_85, x_97);
x_99 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
x_99 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
x_100 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_100, 0, x_99);
lean_ctor_set(x_100, 1, x_98);
@ -17973,7 +17973,7 @@ x_153 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_153, 0, x_143);
lean_ctor_set(x_153, 1, x_152);
x_154 = lean_array_push(x_141, x_153);
x_155 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
x_155 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
x_156 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_156, 0, x_155);
lean_ctor_set(x_156, 1, x_154);

896
stage0/stdlib/Lean/Elab/BuiltinNotation.c generated
View file

File diff suppressed because it is too large Load diff

6
stage0/stdlib/Lean/Elab/Declaration.c generated
View file

@ -189,7 +189,6 @@ lean_object* l_Lean_Elab_Command_expandDeclIdNamespace_x3f_match__1___rarg(lean_
lean_object* l_Lean_Elab_Command_expandMutualPreamble___closed__3;
lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f(lean_object*);
extern lean_object* l_Lean_Parser_Command_open___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__5;
lean_object* l_Lean_Elab_Command_elabCommand(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_sortDeclLevelParams(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_isMutualInductive___boxed(lean_object*);
@ -256,6 +255,7 @@ lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean
extern lean_object* l_Lean_Elab_Command_elabStructure___closed__1;
lean_object* l_Lean_Elab_Command_expandMutualPreamble___closed__5;
lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__5;
lean_object* l_Lean_Elab_Command_expandMutualNamespace_match__2(lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_expandMutualElement___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_getMainModule___rarg(lean_object*, lean_object*);
@ -7131,7 +7131,7 @@ x_57 = l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_268____closed__2;
x_58 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_58, 0, x_57);
lean_ctor_set(x_58, 1, x_56);
x_59 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__5;
x_59 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__5;
x_60 = lean_array_push(x_59, x_58);
x_61 = lean_array_push(x_60, x_26);
x_62 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__46;
@ -7334,7 +7334,7 @@ x_181 = l_Lean_Parser_myMacro____x40_Lean_Parser_Extra___hyg_268____closed__2;
x_182 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_182, 0, x_181);
lean_ctor_set(x_182, 1, x_180);
x_183 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__5;
x_183 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__5;
x_184 = lean_array_push(x_183, x_182);
x_185 = lean_array_push(x_184, x_116);
x_186 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__46;

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

File diff suppressed because it is too large Load diff

14
stage0/stdlib/Lean/Elab/Tactic/Basic.c generated
View file

@ -179,6 +179,7 @@ lean_object* l_Lean_Elab_Tactic_tryCatch___rarg(lean_object*, lean_object*, lean
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalClear(lean_object*);
lean_object* l_Lean_Elab_Tactic_evalFailIfSuccess___closed__3;
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalIntros___closed__1;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__3;
lean_object* l_Lean_Meta_intro(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_tagUntaggedGoals___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalAssumption(lean_object*);
@ -422,6 +423,7 @@ lean_object* l_Lean_Elab_Tactic_focus___rarg___lambda__1___boxed(lean_object*, l
lean_object* l_Lean_Elab_Tactic_tagUntaggedGoals_match__2(lean_object*);
lean_object* l_List_filterAuxM___at_Lean_Elab_Tactic_pruneSolvedGoals___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalFailIfSuccess(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
lean_object* l_Lean_Elab_Tactic_evalIntros_match__1(lean_object*);
lean_object* l_Lean_Meta_isExprMVarAssigned(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_TacticM_run___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -452,7 +454,6 @@ lean_object* l_Lean_Meta_inferType(lean_object*, lean_object*, lean_object*, lea
lean_object* l___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_getIntrosSize___boxed(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed___closed__1;
lean_object* l_Lean_Elab_Tactic_evalAssumption___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__3;
lean_object* l_Std_HashMapImp_find_x3f___at_Lean_Elab_Tactic_evalTactic___spec__5(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_liftTermElabM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_liftMetaTacticAux(lean_object*);
@ -495,7 +496,6 @@ lean_object* l_Lean_indentD(lean_object*);
extern lean_object* l_Lean_Elab_unsupportedSyntaxExceptionId;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_evalTactic___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
lean_object* l_Lean_Elab_Tactic_BacktrackableState_restore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalSubst___closed__1;
lean_object* l_Lean_Elab_Tactic_evalIntros(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -8401,7 +8401,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Elab_Tactic_tacticElabAttribute;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
x_4 = l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
@ -8939,7 +8939,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Elab_Tactic_tacticElabAttribute;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__3;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__3;
x_4 = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
@ -10211,7 +10211,7 @@ x_42 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_42, 0, x_29);
lean_ctor_set(x_42, 1, x_41);
x_43 = lean_array_push(x_27, x_42);
x_44 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
x_44 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
x_45 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_45, 0, x_44);
lean_ctor_set(x_45, 1, x_43);
@ -10412,7 +10412,7 @@ x_137 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_137, 0, x_66);
lean_ctor_set(x_137, 1, x_136);
x_138 = lean_array_push(x_91, x_137);
x_139 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
x_139 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
x_140 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_140, 0, x_139);
lean_ctor_set(x_140, 1, x_138);
@ -14105,7 +14105,7 @@ x_15 = l_Lean_Syntax_getArg(x_1, x_14);
x_16 = lean_unsigned_to_nat(3u);
x_17 = l_Lean_Syntax_getArg(x_1, x_16);
lean_dec(x_1);
x_18 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__3;
x_18 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__3;
lean_inc(x_17);
x_19 = l_Lean_Syntax_isOfKind(x_17, x_18);
if (x_19 == 0)

4
stage0/stdlib/Lean/Meta/AppBuilder.c generated
View file

@ -269,7 +269,7 @@ lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkCongrFunImp___close
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Lean_Meta_mkAppM___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MessageData_arrayExpr_toMessageData(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14019____closed__1;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14025____closed__1;
lean_object* l_Lean_Meta_mkHEqRefl___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___lambda__1___closed__1;
lean_object* l_Lean_Meta_mkAppOptM___at_Lean_Meta_mkDecideProof___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -10908,7 +10908,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkDecIsTrue___closed__2;
x_2 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14019____closed__1;
x_2 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14025____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}

88
stage0/stdlib/Lean/Parser/Term.c generated
View file

@ -27,6 +27,7 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_10790____closed__11;
lean_object* l_Lean_Parser_Term_scoped___closed__2;
lean_object* l_Lean_Parser_Term_explicitUniv___closed__7;
lean_object* l_Lean_Parser_Term_basicFun_formatter___closed__3;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14154____closed__2;
lean_object* l_Lean_Parser_Term_attrInstance_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_nativeDecide___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_sufficesDecl_formatter___closed__1;
@ -1097,6 +1098,7 @@ lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_typeSpec_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Tactic_quot_formatter___closed__1;
lean_object* l_Lean_Parser_Term_structInst_parenthesizer___closed__8;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__3;
lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__17;
lean_object* l_Lean_Parser_Term_ensureTypeOf___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_whereDecls___closed__1;
@ -1710,6 +1712,7 @@ lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1(lean_object*, lean_obje
lean_object* l_Lean_Parser_Term_paren_parenthesizer___closed__10;
lean_object* l_Lean_Parser_Term_scoped;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_11918____closed__7;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__3;
lean_object* l_Lean_Parser_Term_parser_x21_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_fun___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___closed__8;
@ -1882,7 +1885,6 @@ lean_object* l_Lean_Parser_Term_letrec_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Term_namedArgument;
lean_object* l_Lean_Parser_Term_binderTactic___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_dbgTrace___elambda__1___closed__7;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__3;
lean_object* l_Lean_Parser_Term_structInst_parenthesizer___closed__4;
lean_object* l_Lean_Parser_Term_implicitBinder(uint8_t);
lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___closed__7;
@ -1929,7 +1931,6 @@ lean_object* l_Lean_Parser_parserOfStack(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_let_x2a___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Term_anonymousCtor_formatter___closed__1;
extern lean_object* l_Lean_Parser_Tactic_suffices___closed__1;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14019____closed__2;
lean_object* l_Lean_Parser_Term_letDecl___closed__9;
extern lean_object* l_Lean_Parser_Level_ident___closed__1;
lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__21;
@ -2002,6 +2003,7 @@ lean_object* l_Lean_Parser_Term_doubleQuotedName;
lean_object* l___regBuiltin_Lean_Parser_Term_prop_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_borrowed_formatter___closed__1;
lean_object* l_Lean_Parser_Term_typeOf___elambda__1___closed__6;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14025____closed__2;
lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_simpleBinder_formatter___closed__1;
lean_object* l_Lean_Parser_Term_dbgTrace_formatter___closed__4;
@ -2185,10 +2187,10 @@ lean_object* l_Lean_Parser_Term_attrInstance;
lean_object* l_Lean_Parser_Tactic_tacticSeqBracketed___elambda__1___closed__3;
lean_object* l___regBuiltin_Lean_Parser_Term_show_formatter___closed__1;
lean_object* l_Lean_Parser_Term_stateRefT___elambda__1___closed__11;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14019____closed__1;
lean_object* l_Lean_Parser_Term_dynamicQuot_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__9;
lean_object* l_Lean_Parser_Level_quot___closed__7;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14025____closed__1;
lean_object* l___regBuiltinParser_Lean_Parser_Term_fun(lean_object*);
lean_object* l_Lean_Parser_Term_haveAssign___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_funImplicitBinder___closed__3;
@ -2832,6 +2834,7 @@ lean_object* l_Lean_Parser_Term_structInstLVal___closed__8;
lean_object* l_Lean_Parser_Term_letIdDecl___closed__3;
lean_object* l_Lean_Parser_Term_explicit_formatter___closed__2;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_1625____closed__4;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
lean_object* l_Lean_Parser_Term_attrKind_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Term_match___closed__8;
lean_object* l_Lean_Parser_Term_forall___closed__8;
@ -2978,7 +2981,6 @@ lean_object* l_Lean_Parser_Term_emptyC___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Term_have_formatter(lean_object*);
lean_object* l_Lean_Parser_Term_funSimpleBinder___closed__1;
lean_object* l_Lean_Parser_Term_unreachable_parenthesizer___closed__1;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__3;
lean_object* l_Lean_Parser_Term_panic_formatter___closed__1;
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Term___hyg_3590____closed__26;
lean_object* l_Lean_Parser_Term_attrInstance_formatter___closed__1;
@ -3205,7 +3207,6 @@ lean_object* l_Lean_Parser_Term_parenSpecial_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Term_match_formatter___closed__10;
lean_object* l_Lean_Parser_Term_scientific___closed__1;
lean_object* l_Lean_Parser_Term_suffices_parenthesizer___closed__6;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__4;
lean_object* l_Lean_Parser_Term_attrKind___elambda__1___closed__5;
extern lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_2533____closed__5;
lean_object* l_Lean_Parser_Term_letRecDecls___closed__1;
@ -3220,7 +3221,6 @@ lean_object* l_Lean_Parser_Term_explicitUniv_formatter___closed__4;
lean_object* l_Lean_Parser_Term_nomatch___elambda__1___closed__10;
lean_object* l_Lean_Parser_Term_assert_formatter___closed__6;
lean_object* l___regBuiltinParser_Lean_Parser_Term_arrow(lean_object*);
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
lean_object* l_Lean_Parser_Term_paren_parenthesizer___closed__6;
lean_object* l_Lean_Parser_Term_basicFun___closed__9;
lean_object* l___regBuiltinParser_Lean_Parser_Term_namedPattern(lean_object*);
@ -3369,6 +3369,7 @@ lean_object* l_Lean_Parser_Term_letrec___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_matchDiscr_parenthesizer___closed__6;
lean_object* l_Lean_Parser_Term_panic_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_syntheticHole_parenthesizer___closed__2;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__4;
lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__7;
lean_object* l___regBuiltin_Lean_Parser_Term_arrayRef_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_byTactic_parenthesizer___closed__4;
@ -3555,7 +3556,6 @@ lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Term___hyg_3590____closed__
lean_object* l___regBuiltin_Lean_Parser_Term_type_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Term_matchAltsWhereDecls___closed__5;
lean_object* l_Lean_Parser_Term_letDecl___closed__3;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14148____closed__2;
lean_object* l_Lean_Parser_Term_whereDecls___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_doubleQuotedName___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_letrec_formatter___closed__1;
@ -3584,6 +3584,7 @@ lean_object* l_Lean_Parser_Term_nomatch___elambda__1___closed__7;
extern lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_namedPattern___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_attrInstance_parenthesizer___closed__6;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14154____closed__1;
lean_object* l_Lean_Parser_Term_suffices___closed__6;
lean_object* l_Lean_Parser_Term_fun_formatter___closed__4;
lean_object* l_Lean_PrettyPrinter_Formatter_withoutPosition_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -3718,7 +3719,6 @@ lean_object* l_Lean_Parser_termParser_parenthesizer(lean_object*, lean_object*,
lean_object* l_Lean_Parser_Term_letIdLhs_parenthesizer___closed__2;
lean_object* l_Lean_Parser_Term_attributes_formatter___closed__3;
lean_object* l_Lean_Parser_Term_letEqnsDecl___closed__4;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14148____closed__1;
lean_object* l_Lean_Parser_Term_simpleBinderWithoutType_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_whereDecls_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_prop___elambda__1(lean_object*, lean_object*);
@ -4504,7 +4504,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
x_1 = l_Lean_Parser_Tactic_case___closed__9;
x_2 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__3;
x_2 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__3;
x_3 = l_Lean_Parser_Tactic_tacticSeq___closed__3;
x_4 = 0;
x_5 = l_Lean_Parser_nodeWithAntiquot(x_1, x_2, x_3, x_4);
@ -4591,7 +4591,7 @@ lean_inc(x_5);
x_6 = lean_array_get_size(x_5);
lean_dec(x_5);
x_7 = lean_apply_2(x_4, x_1, x_2);
x_8 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
x_8 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
x_9 = l_Lean_Parser_ParserState_mkNode(x_7, x_8, x_6);
return x_9;
}
@ -4603,7 +4603,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__6;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
x_4 = l_Lean_Parser_nodeInfo(x_3, x_2);
return x_4;
}
@ -5218,7 +5218,7 @@ _start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9; lean_object* x_10;
x_6 = l_Lean_Parser_Tactic_case___closed__9;
x_7 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__3;
x_7 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__3;
x_8 = l_Lean_Parser_Tactic_tacticSeq_formatter___closed__3;
x_9 = 0;
x_10 = l_Lean_Parser_nodeWithAntiquot_formatter(x_6, x_7, x_8, x_9, x_1, x_2, x_3, x_4, x_5);
@ -5548,7 +5548,7 @@ lean_object* l_Lean_Parser_Tactic_tacticSeq_parenthesizer(lean_object* x_1, lean
_start:
{
lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9;
x_6 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__3;
x_6 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__3;
x_7 = l_Lean_Parser_Tactic_tacticSeq_parenthesizer___closed__3;
x_8 = 0;
x_9 = l_Lean_Parser_nodeWithAntiquot_parenthesizer___rarg(x_6, x_7, x_8, x_1, x_2, x_3, x_4, x_5);
@ -8195,7 +8195,7 @@ static lean_object* _init_l_Lean_Parser_Term_sorry___elambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14148____closed__2;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14154____closed__2;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -8205,7 +8205,7 @@ static lean_object* _init_l_Lean_Parser_Term_sorry___elambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14148____closed__1;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14154____closed__1;
x_2 = l_Lean_Parser_Term_sorry___elambda__1___closed__1;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -8216,7 +8216,7 @@ static lean_object* _init_l_Lean_Parser_Term_sorry___elambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14148____closed__1;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14154____closed__1;
x_2 = l_String_trim(x_1);
return x_2;
}
@ -8235,7 +8235,7 @@ static lean_object* _init_l_Lean_Parser_Term_sorry___elambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14148____closed__2;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14154____closed__2;
x_2 = l_Lean_Parser_Term_sorry___elambda__1___closed__4;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
@ -8281,7 +8281,7 @@ static lean_object* _init_l_Lean_Parser_Term_sorry___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14148____closed__2;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14154____closed__2;
x_2 = l_Lean_Parser_Term_sorry___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
@ -8342,7 +8342,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_term___u2218_____closed__6;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14148____closed__2;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14154____closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Term_sorry;
x_6 = lean_unsigned_to_nat(0u);
@ -8354,7 +8354,7 @@ static lean_object* _init_l_Lean_Parser_Term_sorry_formatter___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14148____closed__1;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14154____closed__1;
x_2 = l_Lean_Parser_Term_sorry___elambda__1___closed__1;
x_3 = 1;
x_4 = lean_box(x_3);
@ -8369,7 +8369,7 @@ static lean_object* _init_l_Lean_Parser_Term_sorry_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14148____closed__1;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14154____closed__1;
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_symbol_formatter), 6, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -8379,7 +8379,7 @@ static lean_object* _init_l_Lean_Parser_Term_sorry_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14148____closed__2;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14154____closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_sorry_formatter___closed__2;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -8412,7 +8412,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_PrettyPrinter_formatterAttribute;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14148____closed__2;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14154____closed__2;
x_4 = l___regBuiltin_Lean_Parser_Term_sorry_formatter___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
@ -8435,7 +8435,7 @@ static lean_object* _init_l_Lean_Parser_Term_sorry_parenthesizer___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14148____closed__2;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14154____closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
@ -8468,7 +8468,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_PrettyPrinter_parenthesizerAttribute;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14148____closed__2;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14154____closed__2;
x_4 = l___regBuiltin_Lean_Parser_Term_sorry_parenthesizer___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
@ -11478,7 +11478,7 @@ static lean_object* _init_l_Lean_Parser_Term_haveAssign___elambda__1___closed__1
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__4;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__4;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -11488,7 +11488,7 @@ static lean_object* _init_l_Lean_Parser_Term_haveAssign___elambda__1___closed__2
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__3;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__3;
x_2 = l_Lean_Parser_Term_haveAssign___elambda__1___closed__1;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -11530,7 +11530,7 @@ static lean_object* _init_l_Lean_Parser_Term_haveAssign___elambda__1___closed__6
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__4;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__4;
x_2 = l_Lean_Parser_Term_haveAssign___elambda__1___closed__5;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
@ -11588,7 +11588,7 @@ static lean_object* _init_l_Lean_Parser_Term_haveAssign___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__4;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__4;
x_2 = l_Lean_Parser_Term_haveAssign___closed__2;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
@ -12286,7 +12286,7 @@ static lean_object* _init_l_Lean_Parser_Term_haveAssign_formatter___closed__1()
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__3;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__3;
x_2 = l_Lean_Parser_Term_haveAssign___elambda__1___closed__1;
x_3 = 1;
x_4 = lean_box(x_3);
@ -12323,7 +12323,7 @@ static lean_object* _init_l_Lean_Parser_Term_haveAssign_formatter___closed__4()
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__4;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__4;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_haveAssign_formatter___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -12658,7 +12658,7 @@ static lean_object* _init_l_Lean_Parser_Term_haveAssign_parenthesizer___closed__
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15698____closed__4;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_15704____closed__4;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_typeAscription_parenthesizer___closed__2;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
@ -33738,7 +33738,7 @@ static lean_object* _init_l_Lean_Parser_Term_decide___elambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14019____closed__2;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14025____closed__2;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -33748,7 +33748,7 @@ static lean_object* _init_l_Lean_Parser_Term_decide___elambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14019____closed__1;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14025____closed__1;
x_2 = l_Lean_Parser_Term_decide___elambda__1___closed__1;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -33778,7 +33778,7 @@ static lean_object* _init_l_Lean_Parser_Term_decide___elambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14019____closed__2;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14025____closed__2;
x_2 = l_Lean_Parser_Term_decide___elambda__1___closed__4;
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2);
lean_closure_set(x_3, 0, x_1);
@ -33824,7 +33824,7 @@ static lean_object* _init_l_Lean_Parser_Term_decide___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14019____closed__2;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14025____closed__2;
x_2 = l_Lean_Parser_Term_decide___closed__1;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
@ -33885,7 +33885,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_term___u2218_____closed__6;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14019____closed__2;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14025____closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Term_decide;
x_6 = lean_unsigned_to_nat(0u);
@ -33897,7 +33897,7 @@ static lean_object* _init_l_Lean_Parser_Term_decide_formatter___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14019____closed__1;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14025____closed__1;
x_2 = l_Lean_Parser_Term_decide___elambda__1___closed__1;
x_3 = 1;
x_4 = lean_box(x_3);
@ -33922,7 +33922,7 @@ static lean_object* _init_l_Lean_Parser_Term_decide_formatter___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14019____closed__2;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14025____closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_Term_decide_formatter___closed__2;
x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3);
@ -33955,7 +33955,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_PrettyPrinter_formatterAttribute;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14019____closed__2;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14025____closed__2;
x_4 = l___regBuiltin_Lean_Parser_Term_decide_formatter___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
@ -33978,7 +33978,7 @@ static lean_object* _init_l_Lean_Parser_Term_decide_parenthesizer___closed__2()
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14019____closed__2;
x_1 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14025____closed__2;
x_2 = lean_unsigned_to_nat(1024u);
x_3 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3;
x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3);
@ -34011,7 +34011,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_PrettyPrinter_parenthesizerAttribute;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14019____closed__2;
x_3 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14025____closed__2;
x_4 = l___regBuiltin_Lean_Parser_Term_decide_parenthesizer___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
@ -43297,7 +43297,7 @@ lean_object* l_Lean_Parser_Tactic_seq1_formatter(lean_object* x_1, lean_object*
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
x_6 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
x_7 = l_Lean_Parser_Tactic_seq1_formatter___closed__2;
x_8 = l_Lean_PrettyPrinter_Formatter_node_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;
@ -43424,7 +43424,7 @@ lean_object* l_Lean_Parser_Tactic_seq1_parenthesizer(lean_object* x_1, lean_obje
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__2;
x_6 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__2;
x_7 = l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1;
x_8 = l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5);
return x_8;

1586
stage0/stdlib/Lean/Parser/Transform.c generated Normal file
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c generated
View file

@ -190,6 +190,7 @@ lean_object* lean_pretty_printer_parenthesizer_interpret_parser_descr(lean_objec
lean_object* l_Lean_PrettyPrinter_Parenthesizer_parserOfStack_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___closed__3;
lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___lambda__1___closed__1;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__3;
lean_object* l_Lean_PrettyPrinter_parenthesize___closed__3;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkWsBefore_parenthesizer___rarg(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__2(lean_object*);
@ -445,7 +446,6 @@ lean_object* l_Lean_Syntax_MonadTraverser_goUp___at_Lean_PrettyPrinter_Parenthes
lean_object* l_Lean_PrettyPrinter_Parenthesizer_trailingNode_parenthesizer___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_forM_loop___at_Lean_PrettyPrinter_Parenthesizer_parenthesizeCategoryCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_MonadTraverser_getIdx___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__3;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2497____closed__12;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_trailingNode_parenthesizer___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__3;
@ -7673,7 +7673,7 @@ _start:
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_5 = l_Array_empty___closed__1;
x_6 = lean_array_push(x_5, x_1);
x_7 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13707____closed__3;
x_7 = l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_13713____closed__3;
x_8 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_6);

330
stage0/stdlib/Lean/Server/ServerBin.c generated Normal file
View file

@ -0,0 +1,330 @@
// Lean compiler output
// Module: Lean.Server.ServerBin
// Imports: Init Init.System.IO Lean.Server
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* lean_get_stdin(lean_object*);
lean_object* lean_io_error_to_string(lean_object*);
lean_object* _lean_main(lean_object*, lean_object*);
lean_object* lean_get_stderr(lean_object*);
lean_object* l_main___boxed__const__1;
lean_object* l_IO_getStdin___at_main___spec__1(lean_object*);
lean_object* lean_init_search_path(lean_object*, lean_object*);
lean_object* lean_get_stdout(lean_object*);
lean_object* l_IO_FS_Stream_putStrLn___at_Lean_Server_Test_runWithInputFile___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_initAndRunServer(lean_object*, lean_object*, lean_object*);
lean_object* l_IO_getStdin___at_main___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_get_stdin(x_1);
return x_2;
}
}
static lean_object* _init_l_main___boxed__const__1() {
_start:
{
uint32_t x_1; lean_object* x_2;
x_1 = 0;
x_2 = lean_box_uint32(x_1);
return x_2;
}
}
lean_object* _lean_main(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
lean_dec(x_1);
x_3 = lean_get_stdin(x_2);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_ctor_get(x_3, 1);
lean_inc(x_5);
lean_dec(x_3);
x_6 = lean_get_stdout(x_5);
if (lean_obj_tag(x_6) == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_6, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_6, 1);
lean_inc(x_8);
lean_dec(x_6);
x_9 = lean_get_stderr(x_8);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = lean_box(0);
x_13 = lean_init_search_path(x_12, x_11);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15;
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = l_Lean_Server_initAndRunServer(x_4, x_7, x_14);
if (lean_obj_tag(x_15) == 0)
{
uint8_t x_16;
lean_dec(x_10);
x_16 = !lean_is_exclusive(x_15);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18;
x_17 = lean_ctor_get(x_15, 0);
lean_dec(x_17);
x_18 = l_main___boxed__const__1;
lean_ctor_set(x_15, 0, x_18);
return x_15;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_15, 1);
lean_inc(x_19);
lean_dec(x_15);
x_20 = l_main___boxed__const__1;
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
return x_21;
}
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_22 = lean_ctor_get(x_15, 0);
lean_inc(x_22);
x_23 = lean_ctor_get(x_15, 1);
lean_inc(x_23);
lean_dec(x_15);
x_24 = lean_io_error_to_string(x_22);
x_25 = l_IO_FS_Stream_putStrLn___at_Lean_Server_Test_runWithInputFile___spec__1(x_10, x_24, x_23);
if (lean_obj_tag(x_25) == 0)
{
uint8_t x_26;
x_26 = !lean_is_exclusive(x_25);
if (x_26 == 0)
{
lean_object* x_27; lean_object* x_28;
x_27 = lean_ctor_get(x_25, 0);
lean_dec(x_27);
x_28 = l_main___boxed__const__1;
lean_ctor_set(x_25, 0, x_28);
return x_25;
}
else
{
lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_29 = lean_ctor_get(x_25, 1);
lean_inc(x_29);
lean_dec(x_25);
x_30 = l_main___boxed__const__1;
x_31 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_29);
return x_31;
}
}
else
{
uint8_t x_32;
x_32 = !lean_is_exclusive(x_25);
if (x_32 == 0)
{
return x_25;
}
else
{
lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_33 = lean_ctor_get(x_25, 0);
x_34 = lean_ctor_get(x_25, 1);
lean_inc(x_34);
lean_inc(x_33);
lean_dec(x_25);
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_33);
lean_ctor_set(x_35, 1, x_34);
return x_35;
}
}
}
}
else
{
uint8_t x_36;
lean_dec(x_10);
lean_dec(x_7);
lean_dec(x_4);
x_36 = !lean_is_exclusive(x_13);
if (x_36 == 0)
{
return x_13;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_37 = lean_ctor_get(x_13, 0);
x_38 = lean_ctor_get(x_13, 1);
lean_inc(x_38);
lean_inc(x_37);
lean_dec(x_13);
x_39 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_39, 0, x_37);
lean_ctor_set(x_39, 1, x_38);
return x_39;
}
}
}
else
{
uint8_t x_40;
lean_dec(x_7);
lean_dec(x_4);
x_40 = !lean_is_exclusive(x_9);
if (x_40 == 0)
{
return x_9;
}
else
{
lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_41 = lean_ctor_get(x_9, 0);
x_42 = lean_ctor_get(x_9, 1);
lean_inc(x_42);
lean_inc(x_41);
lean_dec(x_9);
x_43 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_43, 0, x_41);
lean_ctor_set(x_43, 1, x_42);
return x_43;
}
}
}
else
{
uint8_t x_44;
lean_dec(x_4);
x_44 = !lean_is_exclusive(x_6);
if (x_44 == 0)
{
return x_6;
}
else
{
lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_45 = lean_ctor_get(x_6, 0);
x_46 = lean_ctor_get(x_6, 1);
lean_inc(x_46);
lean_inc(x_45);
lean_dec(x_6);
x_47 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_47, 0, x_45);
lean_ctor_set(x_47, 1, x_46);
return x_47;
}
}
}
else
{
uint8_t x_48;
x_48 = !lean_is_exclusive(x_3);
if (x_48 == 0)
{
return x_3;
}
else
{
lean_object* x_49; lean_object* x_50; lean_object* x_51;
x_49 = lean_ctor_get(x_3, 0);
x_50 = lean_ctor_get(x_3, 1);
lean_inc(x_50);
lean_inc(x_49);
lean_dec(x_3);
x_51 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_51, 0, x_49);
lean_ctor_set(x_51, 1, x_50);
return x_51;
}
}
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Init_System_IO(lean_object*);
lean_object* initialize_Lean_Server(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Server_ServerBin(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_System_IO(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Server(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_main___boxed__const__1 = _init_l_main___boxed__const__1();
lean_mark_persistent(l_main___boxed__const__1);
return lean_io_result_mk_ok(lean_box(0));
}
void lean_initialize();
#if defined(WIN32) || defined(_WIN32)
#include <windows.h>
#endif
int main(int argc, char ** argv) {
#if defined(WIN32) || defined(_WIN32)
SetErrorMode(SEM_FAILCRITICALERRORS);
#endif
lean_object* in; lean_object* res;
lean_initialize();
res = initialize_Lean_Server_ServerBin(lean_io_mk_world());
lean_io_mark_end_initialization();
if (lean_io_result_is_ok(res)) {
lean_dec_ref(res);
lean_init_task_manager();
in = lean_box(0);
int i = argc;
while (i > 1) {
lean_object* n;
i--;
n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);
in = n;
}
res = _lean_main(in, lean_io_mk_world());
}
if (lean_io_result_is_ok(res)) {
int ret = lean_unbox(lean_io_result_get_value(res));
lean_dec_ref(res);
return ret;
} else {
lean_io_result_show_error(res);
lean_dec_ref(res);
return 1;
}
}
#ifdef __cplusplus
}
#endif