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-10-10 16:17:28 -07:00
parent c5e3da89e8
commit a258734134
9 changed files with 9948 additions and 5205 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -565,6 +565,9 @@ private partial def elabAppFn : Syntax → List LVal → Array NamedArg → Arra
| `($(e).$idx:fieldIdx) =>
let idx := idx.isFieldIdx?.get!;
elabAppFn e (LVal.fieldIdx idx :: lvals) namedArgs args expectedType? explicit overloaded acc
| `($e $.$field) => do
f ← `($(e).$field);
elabAppFn f lvals namedArgs args expectedType? explicit overloaded acc
| `($(e).$field:ident) =>
let newLVals := field.getId.eraseMacroScopes.components.map (fun n => LVal.fieldName (toString n));
elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit overloaded acc
@ -692,6 +695,7 @@ fun stx expectedType? => elabAppAux stx #[] #[] expectedType?
@[builtinTermElab ident] def elabIdent : TermElab := elabAtom
@[builtinTermElab namedPattern] def elabNamedPattern : TermElab := elabAtom
@[builtinTermElab explicitUniv] def elabExplicitUniv : TermElab := elabAtom
@[builtinTermElab dollarProj] def expandDollarProj : TermElab := elabAtom
@[builtinTermElab explicit] def elabExplicit : TermElab :=
fun stx expectedType? => match_syntax stx with

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

@ -20,11 +20,6 @@ fun stx => match_syntax stx with
| `($f $ $a) => `($f $a)
| _ => Macro.throwUnsupported
@[builtinMacro Lean.Parser.Term.dollarProj] def expandDollarProj : Macro :=
fun stx => match_syntax stx with
| `($term $.$field) => `($(term).$field)
| _ => Macro.throwUnsupported
@[builtinMacro Lean.Parser.Term.if] def expandIf : Macro :=
fun stx => match_syntax stx with
| `(if $h : $cond then $t else $e) => `(dite $cond (fun $h:ident => $t) (fun $h:ident => $e))

129
stage0/src/Lean/Elab/Match.lean generated
View file

@ -72,11 +72,28 @@ match e with
| Expr.fvar fvarId _ => do localDecl ← getLocalDecl fvarId; pure localDecl.userName
| _ => mkFreshBinderName
-- `expandNonAtomicDiscrs?` create auxiliary variables with base name `_discr`
private def isAuxDiscrName (n : Name) : Bool :=
n.eraseMacroScopes == `_discr
-- See expandNonAtomicDiscrs?
private def elabAtomicDiscr (discr : Syntax) : TermElabM Expr := do
let term := discr.getArg 1;
local? ← isLocalIdent? term;
match local? with
| some e@(Expr.fvar fvarId _) => do
localDecl ← getLocalDecl fvarId;
if !isAuxDiscrName localDecl.userName then
pure e -- it is not an auxiliary local created by `expandNonAtomicDiscrs?`
else
pure localDecl.value
| _ => throwErrorAt discr "unexpected discriminant"
private def elabMatchTypeAndDiscrsAux (discrStxs : Array Syntax) : Nat → Array Expr → Expr → Array MatchAltView → TermElabM (Array Expr × Expr × Array MatchAltView)
| 0, discrs, matchType, matchAltViews => pure (discrs.reverse, matchType, matchAltViews)
| i+1, discrs, matchType, matchAltViews => do
let discrStx := discrStxs.get! i;
discr ← elabTerm (discrStx.getArg 1) none;
discr ← elabAtomicDiscr discrStx;
discr ← instantiateMVars discr;
discrType ← inferType discr;
discrType ← instantiateMVars discrType;
@ -738,12 +755,100 @@ let r := mkAppN r rhss;
trace `Elab.match fun _ => "result: " ++ r;
pure r
private def getDiscrs (matchStx : Syntax) : Array Syntax :=
(matchStx.getArg 1).getArgs.getSepElems
private def getMatchOptType (matchStx : Syntax) : Syntax :=
matchStx.getArg 2
private def expandNonAtomicDiscrsAux (matchStx : Syntax) : List Syntax → Array Syntax → TermElabM Syntax
| [], discrsNew =>
let discrs := mkSepStx discrsNew (mkAtomFrom matchStx ", ");
pure $ matchStx.setArg 1 discrs
| discr :: discrs, discrsNew => do
-- Recall that
-- matchDiscr := parser! optional (ident >> ":") >> termParser
let term := discr.getArg 1;
local? ← isLocalIdent? term;
match local? with
| some _ => expandNonAtomicDiscrsAux discrs (discrsNew.push discr)
| none => withFreshMacroScope do
d ← `(_discr);
unless (isAuxDiscrName d.getId) $ -- Use assertion?
throwError "unexpected internal auxiliary discriminant name";
let discrNew := discr.setArg 1 d;
r ← expandNonAtomicDiscrsAux discrs (discrsNew.push discrNew);
`(let _discr := $term; $r)
private def expandNonAtomicDiscrs? (matchStx : Syntax) : TermElabM (Option Syntax) :=
let matchOptType := getMatchOptType matchStx;
if matchOptType.isNone then do
let discrs := getDiscrs matchStx;
allLocal ← discrs.allM fun discr => Option.isSome <$> isLocalIdent? (discr.getArg 1);
if allLocal then
pure none
else
some <$> expandNonAtomicDiscrsAux matchStx discrs.toList #[]
else
-- We do not pull non atomic discriminants when match type is provided explicitly by the user
pure none
private def waitExpectedType (expectedType? : Option Expr) : TermElabM Expr := do
tryPostponeIfNoneOrMVar expectedType?;
match expectedType? with
| some expectedType => pure expectedType
| none => mkFreshTypeMVar
private def tryPostponeIfDiscrTypeIsMVar (matchStx : Syntax) : TermElabM Unit :=
-- We don't wait for the discriminants types when match type is provided by user
when (getMatchOptType matchStx).isNone do
let discrs := getDiscrs matchStx;
discrs.forM fun discr => do
let term := discr.getArg 1;
local? ← isLocalIdent? term;
match local? with
| none => throwErrorAt discr "unexpected discriminant" -- see `expandNonAtomicDiscrs?
| some d => do
dType ← inferType d;
tryPostponeIfMVar dType
/-
We (try to) elaborate a `match` only when the expected type is available.
If the `matchType` has not been provided by the user, we also try to postpone elaboration if the type
of a discriminant is not available. That is, it is of the form `(?m ...)`.
We use `expandNonAtomicDiscrs?` to make sure all discriminants are local variables.
This is a standard trick we use in the elaborator, and it is also used to elaborate structure instances.
Suppose, we are trying to elaborate
```
match g x with
| ... => ...
```
`expandNonAtomicDiscrs?` converts it intro
```
let _discr := g x
match _discr with
| ... => ...
```
Thus, at `tryPostponeIfDiscrTypeIsMVar` we only need to check whether the type of `_discr` is not of the form `(?m ...)`.
Note that, the auxiliary variable `_discr` is expanded at `elabAtomicDiscr`.
This elaboration technique is needed to elaborate terms such as:
```lean
xs.filter fun (a, b) => a > b
```
which are syntax sugar for
```lean
List.filter (fun p => match p with | (a, b) => a > b) xs
```
When we visit `match p with | (a, b) => a > b`, we don't know the type of `p` yet.
-/
private def waitExpectedTypeAndDiscrs (matchStx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
tryPostponeIfNoneOrMVar expectedType?;
tryPostponeIfDiscrTypeIsMVar matchStx;
match expectedType? with
| some expectedType => pure expectedType
| none => mkFreshTypeMVar
/-
```
parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
@ -751,10 +856,10 @@ parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> ma
Remark the `optIdent` must be `none` at `matchDiscr`. They are expanded by `expandMatchDiscr?`.
-/
private def elabMatchCore (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
expectedType ← waitExpectedType expectedType?;
let discrStxs := (stx.getArg 1).getArgs.getSepElems.map fun d => d;
let altViews := getMatchAlts stx;
let matchOptType := stx.getArg 2;
expectedType ← waitExpectedTypeAndDiscrs stx expectedType?;
let discrStxs := (getDiscrs stx).map fun d => d;
let altViews := getMatchAlts stx;
let matchOptType := getMatchOptType stx;
elabMatchAux discrStxs altViews matchOptType expectedType
-- parser! "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
@ -765,11 +870,15 @@ fun stx expectedType? => match_syntax stx with
| `(match $discr:term : $type with $y:ident => $rhs:term) => expandSimpleMatchWithType stx discr y type rhs expectedType?
| `(match $discr:term : $type with | $y:ident => $rhs:term) => expandSimpleMatchWithType stx discr y type rhs expectedType?
| _ => do
let discrs := (stx.getArg 1).getArgs;
let matchOptType := stx.getArg 2;
when (!matchOptType.isNone && discrs.getSepElems.any fun d => !(d.getArg 0).isNone) $
throwErrorAt matchOptType "match expected type should not be provided when discriminants with equality proofs are used";
elabMatchCore stx expectedType?
stxNew? ← expandNonAtomicDiscrs? stx;
match stxNew? with
| some stxNew => withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
| none => do
let discrs := getDiscrs stx;
let matchOptType := getMatchOptType stx;
when (!matchOptType.isNone && discrs.any fun d => !(d.getArg 0).isNone) $
throwErrorAt matchOptType "match expected type should not be provided when discriminants with equality proofs are used";
elabMatchCore stx expectedType?
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Elab.match;

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

File diff suppressed because it is too large Load diff

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

@ -110,7 +110,6 @@ lean_object* l___regBuiltin_Lean_Elab_Term_expandSorry___closed__3;
lean_object* l_Lean_Elab_Term_expandModN___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandPow___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandOrM___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_expandDollarProj(lean_object*);
extern lean_object* l___private_Lean_Elab_Quotation_6__compileStxMatch___main___closed__13;
extern lean_object* l_Array_empty___closed__1;
lean_object* l_Lean_Elab_Term_expandAssert___closed__12;
@ -207,7 +206,6 @@ extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Macros___hyg_464____c
lean_object* l___regBuiltin_Lean_Elab_Term_expandMap___closed__2;
extern lean_object* l___private_Lean_Elab_Quotation_8__letBindRhss___main___closed__13;
lean_object* l_Lean_Elab_Term_expandseqLeft(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandDollarProj(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_expandDiv___closed__2;
lean_object* l___private_Lean_Elab_BuiltinNotation_1__elabParserMacroAux___closed__16;
lean_object* l___regBuiltin_Lean_Elab_Term_expandAnd(lean_object*);
@ -361,7 +359,6 @@ lean_object* l___regBuiltin_Lean_Elab_Term_expandEquiv___closed__1;
lean_object* l_Lean_Elab_Term_expandDbgTrace___closed__3;
lean_object* l___regBuiltin_Lean_Elab_Term_expandLE___closed__2;
extern lean_object* l_Lean_strLitKind___closed__2;
lean_object* l_Lean_Elab_Term_expandDollarProj___closed__4;
lean_object* l_Lean_Elab_Term_expandBNot___closed__1;
lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__8;
lean_object* l_Lean_Elab_Term_expandIf___closed__9;
@ -432,7 +429,6 @@ lean_object* l___private_Lean_Elab_BuiltinNotation_4__elabClosedTerm___closed__3
lean_object* l___regBuiltin_Lean_Elab_Term_elabPanic___closed__2;
lean_object* l_Lean_Elab_Term_expandAssert___closed__13;
lean_object* l_Lean_Elab_Term_expandMod___closed__3;
lean_object* l___regBuiltin_Lean_Elab_Term_expandDollarProj___closed__1;
lean_object* l_Lean_compileDecl___at_Lean_Elab_Term_declareTacticSyntax___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabPanic___closed__11;
lean_object* l_Lean_Elab_Term_expandDiv___closed__3;
@ -479,13 +475,11 @@ lean_object* l___regBuiltin_Lean_Elab_Term_expandEquiv___closed__3;
lean_object* l_Lean_Elab_Term_ExpandFComp___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkAtomFrom(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_expandNot___closed__1;
lean_object* l_Lean_Elab_Term_expandDollarProj___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_BuiltinNotation_1__elabParserMacroAux___closed__7;
lean_object* l_Lean_Elab_Term_expandBOr___closed__1;
lean_object* l_Lean_Elab_Term_ExpandFComp___closed__1;
lean_object* l___regBuiltin_Lean_Elab_Term_expandIff___closed__3;
lean_object* l_Lean_Elab_Term_expandModN___closed__2;
lean_object* l_Lean_Elab_Term_expandDollarProj___closed__1;
lean_object* l_Lean_Elab_Term_expandSubtype___closed__3;
lean_object* l_Lean_Elab_Term_expandEq___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_expandModN___closed__3;
@ -543,7 +537,6 @@ lean_object* l_Lean_Elab_Term_expandEmptyC___closed__7;
extern lean_object* l_Lean_Meta_evalNat___main___closed__9;
lean_object* l___regBuiltin_Lean_Elab_Term_expandCons(lean_object*);
lean_object* l_Lean_Elab_Term_expandMap___closed__2;
lean_object* l_Lean_Elab_Term_expandDollarProj___closed__3;
lean_object* l_Lean_Elab_Term_expandNot(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandBind(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandAssert___closed__14;
@ -608,7 +601,6 @@ lean_object* l_Lean_Elab_getRefPos___at_Lean_Elab_Term_elabPanic___spec__2___rar
lean_object* l_Lean_Expr_consumeMData___main(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_expandCons___closed__2;
lean_object* l_Lean_Elab_Term_ExpandFComp___closed__3;
lean_object* l_Lean_Elab_Term_expandDollarProj___closed__2;
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__3;
lean_object* l___regBuiltin_Lean_Elab_Term_expandEq___closed__1;
extern lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__9;
@ -684,7 +676,6 @@ lean_object* l___private_Lean_Elab_BuiltinNotation_1__elabParserMacroAux___close
lean_object* l___regBuiltin_Lean_Elab_Term_expandIf___closed__1;
lean_object* l___private_Lean_Elab_BuiltinNotation_2__elabTParserMacroAux___closed__10;
lean_object* l_Lean_Elab_Term_expandMap___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Expr_ctorName___closed__11;
extern lean_object* l___private_Lean_Elab_Quotation_2__quoteSyntax___main___closed__39;
lean_object* l_Lean_Elab_Term_expandMap___closed__1;
lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__7;
@ -951,135 +942,6 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l_Lean_Elab_Term_expandDollarProj___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("dollarProj");
return x_1;
}
}
lean_object* _init_l_Lean_Elab_Term_expandDollarProj___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l_Lean_Elab_Term_expandDollarProj___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Elab_Term_expandDollarProj___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l_Lean_Expr_ctorName___closed__11;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Elab_Term_expandDollarProj___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_SourceInfo_inhabited___closed__1;
x_2 = l_System_FilePath_dirName___closed__1;
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Term_expandDollarProj(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = l_Lean_Elab_Term_expandDollarProj___closed__2;
lean_inc(x_1);
x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7;
lean_dec(x_1);
x_6 = lean_box(1);
x_7 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_3);
return x_7;
}
else
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_8 = l_Lean_Syntax_getArgs(x_1);
x_9 = lean_array_get_size(x_8);
lean_dec(x_8);
x_10 = lean_unsigned_to_nat(3u);
x_11 = lean_nat_dec_eq(x_9, x_10);
lean_dec(x_9);
if (x_11 == 0)
{
lean_object* x_12; lean_object* x_13;
lean_dec(x_1);
x_12 = lean_box(1);
x_13 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_13, 0, x_12);
lean_ctor_set(x_13, 1, x_3);
return x_13;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_14 = lean_unsigned_to_nat(0u);
x_15 = l_Lean_Syntax_getArg(x_1, x_14);
x_16 = lean_unsigned_to_nat(2u);
x_17 = l_Lean_Syntax_getArg(x_1, x_16);
lean_dec(x_1);
x_18 = l_Array_empty___closed__1;
x_19 = lean_array_push(x_18, x_15);
x_20 = l_Lean_Elab_Term_expandDollarProj___closed__4;
x_21 = lean_array_push(x_19, x_20);
x_22 = lean_array_push(x_21, x_17);
x_23 = l_Lean_Elab_Term_expandDollarProj___closed__3;
x_24 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_22);
x_25 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_3);
return x_25;
}
}
}
}
lean_object* l_Lean_Elab_Term_expandDollarProj___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Elab_Term_expandDollarProj(x_1, x_2, x_3);
lean_dec(x_2);
return x_4;
}
}
lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandDollarProj___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_expandDollarProj___boxed), 3, 0);
return x_1;
}
}
lean_object* l___regBuiltin_Lean_Elab_Term_expandDollarProj(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Elab_macroAttribute;
x_3 = l_Lean_Elab_Term_expandDollarProj___closed__2;
x_4 = l___regBuiltin_Lean_Elab_Term_expandDollarProj___closed__1;
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l_Lean_Elab_Term_expandIf___closed__1() {
_start:
{
@ -11987,19 +11849,6 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_expandDollar___closed__1);
res = l___regBuiltin_Lean_Elab_Term_expandDollar(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_expandDollarProj___closed__1 = _init_l_Lean_Elab_Term_expandDollarProj___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_expandDollarProj___closed__1);
l_Lean_Elab_Term_expandDollarProj___closed__2 = _init_l_Lean_Elab_Term_expandDollarProj___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_expandDollarProj___closed__2);
l_Lean_Elab_Term_expandDollarProj___closed__3 = _init_l_Lean_Elab_Term_expandDollarProj___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_expandDollarProj___closed__3);
l_Lean_Elab_Term_expandDollarProj___closed__4 = _init_l_Lean_Elab_Term_expandDollarProj___closed__4();
lean_mark_persistent(l_Lean_Elab_Term_expandDollarProj___closed__4);
l___regBuiltin_Lean_Elab_Term_expandDollarProj___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_expandDollarProj___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_expandDollarProj___closed__1);
res = l___regBuiltin_Lean_Elab_Term_expandDollarProj(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Term_expandIf___closed__1 = _init_l_Lean_Elab_Term_expandIf___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_expandIf___closed__1);
l_Lean_Elab_Term_expandIf___closed__2 = _init_l_Lean_Elab_Term_expandIf___closed__2();

191
stage0/stdlib/Lean/Elab/Do.c generated
View file

@ -244,7 +244,6 @@ lean_object* l_Lean_Elab_Term_Do_hasExitPointPred___main___at_Lean_Elab_Term_Do_
lean_object* lean_nat_add(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_elabLetDeclCore___closed__2;
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__2___rarg(lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49;
uint8_t l_Array_anyRangeMAux___main___at_Lean_Elab_Term_Do_hasTerminalAction___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_elabDo___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_mkFreshJP(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -482,6 +481,7 @@ lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToC
lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__46;
lean_object* l_Lean_Elab_Term_Do_toMessageDataAux___main___closed__14;
lean_object* l_Lean_Elab_Term_Do_extendUpdatedVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Elab_App_22__elabAppFn___main___closed__9;
lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTermCore___closed__5;
lean_object* l___private_Lean_Elab_Do_15__mkMonadAlias___closed__1;
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -667,7 +667,6 @@ extern lean_object* l___regBuiltin_Lean_Elab_Term_elabEnsureExpectedType___close
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_mkForInBody___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_mkPureUnitAction(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_seqToTermCore___closed__1;
extern lean_object* l___private_Lean_Elab_App_22__elabAppFn___main___closed__13;
lean_object* l_Lean_Elab_Term_Do_ToTerm_reassignToTerm(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isMVar(lean_object*);
extern lean_object* l_Lean_Meta_caseValueAux___lambda__5___closed__8;
@ -683,6 +682,7 @@ lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doForToCode___closed__13;
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
extern lean_object* l_Lean_SourceInfo_inhabited___closed__1;
lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_ensureEOS(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Elab_App_22__elabAppFn___main___closed__14;
lean_object* l_Lean_Elab_Term_Do_getDoReassignVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_mkAuxDeclFor___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_mkFreshJP_x27___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -889,7 +889,6 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__21;
lean_object* l_Lean_Elab_Term_Do_toMessageDataAux___main___closed__6;
lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTermCore___closed__2;
extern lean_object* l_IO_Prim_fopenFlags___closed__1;
extern lean_object* l_System_FilePath_dirName___closed__1;
lean_object* l_Lean_Elab_Term_Do_ToTerm_mkNestedKind(uint8_t, uint8_t, uint8_t);
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__23;
@ -25268,32 +25267,30 @@ return x_3;
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__34() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("2");
return x_1;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__35() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_SourceInfo_inhabited___closed__1;
x_2 = l_System_FilePath_dirName___closed__1;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__34;
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__35() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("2");
return x_1;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__36() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_SourceInfo_inhabited___closed__1;
x_1 = l_Array_empty___closed__1;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__35;
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
@ -25301,25 +25298,15 @@ lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__37
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_empty___closed__1;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__36;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__38() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_fieldIdxKind___closed__2;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__37;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__36;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39() {
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__38() {
_start:
{
lean_object* x_1;
@ -25327,17 +25314,17 @@ x_1 = lean_mk_string("doReturn");
return x_1;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40() {
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkAppStx___closed__6;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__38;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__41() {
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -25349,17 +25336,17 @@ lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42() {
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__41() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_empty___closed__1;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__41;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__43() {
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42() {
_start:
{
lean_object* x_1;
@ -25367,41 +25354,41 @@ x_1 = lean_mk_string("1");
return x_1;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__44() {
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__43() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_SourceInfo_inhabited___closed__1;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__43;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42;
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__44() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_empty___closed__1;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__43;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__45() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Array_empty___closed__1;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__44;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__46() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_fieldIdxKind___closed__2;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__45;
x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__44;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__47() {
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__46() {
_start:
{
lean_object* x_1; lean_object* x_2;
@ -25410,13 +25397,13 @@ x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__48() {
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__47() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_IO_Prim_fopenFlags___closed__4;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__47;
x_3 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__46;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -25424,7 +25411,7 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49() {
lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__48() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -25982,12 +25969,12 @@ x_317 = lean_array_push(x_316, x_296);
x_318 = lean_array_push(x_317, x_296);
x_319 = l_Array_myMacro____x40_Init_Data_Array_Macros___hyg_464____closed__14;
x_320 = lean_array_push(x_318, x_319);
x_321 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__34;
x_321 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__14;
x_322 = lean_array_push(x_295, x_321);
x_323 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__38;
x_323 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__37;
lean_inc(x_322);
x_324 = lean_array_push(x_322, x_323);
x_325 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__13;
x_325 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__9;
x_326 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_326, 0, x_325);
lean_ctor_set(x_326, 1, x_324);
@ -26007,7 +25994,7 @@ x_335 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_335, 0, x_313);
lean_ctor_set(x_335, 1, x_334);
x_336 = lean_array_push(x_315, x_335);
x_337 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__46;
x_337 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__45;
x_338 = lean_array_push(x_322, x_337);
x_339 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_339, 0, x_325);
@ -26016,9 +26003,9 @@ x_340 = lean_array_push(x_294, x_339);
x_341 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_341, 0, x_313);
lean_ctor_set(x_341, 1, x_340);
x_342 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42;
x_342 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__41;
x_343 = lean_array_push(x_342, x_341);
x_344 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40;
x_344 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39;
x_345 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_345, 0, x_344);
lean_ctor_set(x_345, 1, x_343);
@ -26102,9 +26089,9 @@ x_390 = lean_array_push(x_369, x_389);
x_391 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_391, 0, x_388);
lean_ctor_set(x_391, 1, x_370);
x_392 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42;
x_392 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__41;
x_393 = lean_array_push(x_392, x_391);
x_394 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40;
x_394 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39;
x_395 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_395, 0, x_394);
lean_ctor_set(x_395, 1, x_393);
@ -26200,12 +26187,12 @@ x_445 = lean_array_push(x_444, x_424);
x_446 = lean_array_push(x_445, x_424);
x_447 = l_Array_myMacro____x40_Init_Data_Array_Macros___hyg_464____closed__14;
x_448 = lean_array_push(x_446, x_447);
x_449 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__34;
x_449 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__14;
x_450 = lean_array_push(x_423, x_449);
x_451 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__38;
x_451 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__37;
lean_inc(x_450);
x_452 = lean_array_push(x_450, x_451);
x_453 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__13;
x_453 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__9;
x_454 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_454, 0, x_453);
lean_ctor_set(x_454, 1, x_452);
@ -26225,7 +26212,7 @@ x_463 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_463, 0, x_441);
lean_ctor_set(x_463, 1, x_462);
x_464 = lean_array_push(x_443, x_463);
x_465 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__46;
x_465 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__45;
x_466 = lean_array_push(x_450, x_465);
x_467 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_467, 0, x_453);
@ -26234,9 +26221,9 @@ x_468 = lean_array_push(x_422, x_467);
x_469 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_469, 0, x_441);
lean_ctor_set(x_469, 1, x_468);
x_470 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42;
x_470 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__41;
x_471 = lean_array_push(x_470, x_469);
x_472 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40;
x_472 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39;
x_473 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_473, 0, x_472);
lean_ctor_set(x_473, 1, x_471);
@ -26322,9 +26309,9 @@ x_519 = lean_array_push(x_498, x_518);
x_520 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_520, 0, x_517);
lean_ctor_set(x_520, 1, x_499);
x_521 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42;
x_521 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__41;
x_522 = lean_array_push(x_521, x_520);
x_523 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40;
x_523 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39;
x_524 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_524, 0, x_523);
lean_ctor_set(x_524, 1, x_522);
@ -26507,9 +26494,9 @@ x_623 = lean_array_push(x_551, x_622);
x_624 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_624, 0, x_570);
lean_ctor_set(x_624, 1, x_594);
x_625 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42;
x_625 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__41;
x_626 = lean_array_push(x_625, x_624);
x_627 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40;
x_627 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39;
x_628 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_628, 0, x_627);
lean_ctor_set(x_628, 1, x_626);
@ -26800,9 +26787,9 @@ x_790 = lean_array_push(x_718, x_789);
x_791 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_791, 0, x_737);
lean_ctor_set(x_791, 1, x_761);
x_792 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42;
x_792 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__41;
x_793 = lean_array_push(x_792, x_791);
x_794 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40;
x_794 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39;
x_795 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_795, 0, x_794);
lean_ctor_set(x_795, 1, x_793);
@ -27021,12 +27008,12 @@ x_910 = lean_array_push(x_909, x_889);
x_911 = lean_array_push(x_910, x_889);
x_912 = l_Array_myMacro____x40_Init_Data_Array_Macros___hyg_464____closed__14;
x_913 = lean_array_push(x_911, x_912);
x_914 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__34;
x_914 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__14;
x_915 = lean_array_push(x_888, x_914);
x_916 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__38;
x_916 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__37;
lean_inc(x_915);
x_917 = lean_array_push(x_915, x_916);
x_918 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__13;
x_918 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__9;
x_919 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_919, 0, x_918);
lean_ctor_set(x_919, 1, x_917);
@ -27056,7 +27043,7 @@ lean_ctor_set(x_934, 1, x_932);
lean_ctor_set(x_934, 2, x_931);
lean_ctor_set(x_934, 3, x_933);
x_935 = lean_array_push(x_887, x_934);
x_936 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__46;
x_936 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__45;
x_937 = lean_array_push(x_915, x_936);
x_938 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_938, 0, x_918);
@ -27208,12 +27195,12 @@ x_1016 = lean_array_push(x_1015, x_995);
x_1017 = lean_array_push(x_1016, x_995);
x_1018 = l_Array_myMacro____x40_Init_Data_Array_Macros___hyg_464____closed__14;
x_1019 = lean_array_push(x_1017, x_1018);
x_1020 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__34;
x_1020 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__14;
x_1021 = lean_array_push(x_994, x_1020);
x_1022 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__38;
x_1022 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__37;
lean_inc(x_1021);
x_1023 = lean_array_push(x_1021, x_1022);
x_1024 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__13;
x_1024 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__9;
x_1025 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_1025, 0, x_1024);
lean_ctor_set(x_1025, 1, x_1023);
@ -27243,7 +27230,7 @@ lean_ctor_set(x_1040, 1, x_1038);
lean_ctor_set(x_1040, 2, x_1037);
lean_ctor_set(x_1040, 3, x_1039);
x_1041 = lean_array_push(x_993, x_1040);
x_1042 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__46;
x_1042 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__45;
x_1043 = lean_array_push(x_1021, x_1042);
x_1044 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_1044, 0, x_1024);
@ -28158,9 +28145,9 @@ lean_ctor_set(x_1549, 1, x_1547);
lean_ctor_set(x_1549, 2, x_1546);
lean_ctor_set(x_1549, 3, x_1548);
x_1550 = lean_array_push(x_1447, x_1549);
x_1551 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49;
x_1551 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__48;
x_1552 = l_Lean_addMacroScope(x_1440, x_1551, x_1439);
x_1553 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__48;
x_1553 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__47;
x_1554 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_1554, 0, x_1444);
lean_ctor_set(x_1554, 1, x_1553);
@ -28185,9 +28172,9 @@ x_1563 = lean_array_push(x_1562, x_1503);
x_1564 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_1564, 0, x_1466);
lean_ctor_set(x_1564, 1, x_1555);
x_1565 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42;
x_1565 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__41;
x_1566 = lean_array_push(x_1565, x_1564);
x_1567 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40;
x_1567 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39;
x_1568 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_1568, 0, x_1567);
lean_ctor_set(x_1568, 1, x_1566);
@ -28451,9 +28438,9 @@ lean_ctor_set(x_1713, 1, x_1711);
lean_ctor_set(x_1713, 2, x_1710);
lean_ctor_set(x_1713, 3, x_1712);
x_1714 = lean_array_push(x_1611, x_1713);
x_1715 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49;
x_1715 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__48;
x_1716 = l_Lean_addMacroScope(x_1604, x_1715, x_1603);
x_1717 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__48;
x_1717 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__47;
x_1718 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_1718, 0, x_1608);
lean_ctor_set(x_1718, 1, x_1717);
@ -28478,9 +28465,9 @@ x_1727 = lean_array_push(x_1726, x_1667);
x_1728 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_1728, 0, x_1630);
lean_ctor_set(x_1728, 1, x_1719);
x_1729 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42;
x_1729 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__41;
x_1730 = lean_array_push(x_1729, x_1728);
x_1731 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40;
x_1731 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39;
x_1732 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_1732, 0, x_1731);
lean_ctor_set(x_1732, 1, x_1730);
@ -28759,9 +28746,9 @@ lean_ctor_set(x_1883, 0, x_1795);
lean_ctor_set(x_1883, 1, x_1882);
x_1884 = lean_array_push(x_1776, x_1883);
x_1885 = lean_array_push(x_1884, x_1832);
x_1886 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42;
x_1886 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__41;
x_1887 = lean_array_push(x_1886, x_1855);
x_1888 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40;
x_1888 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39;
x_1889 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_1889, 0, x_1888);
lean_ctor_set(x_1889, 1, x_1887);
@ -29116,9 +29103,9 @@ lean_ctor_set(x_2083, 0, x_1995);
lean_ctor_set(x_2083, 1, x_2082);
x_2084 = lean_array_push(x_1976, x_2083);
x_2085 = lean_array_push(x_2084, x_2032);
x_2086 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42;
x_2086 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__41;
x_2087 = lean_array_push(x_2086, x_2055);
x_2088 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40;
x_2088 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39;
x_2089 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_2089, 0, x_2088);
lean_ctor_set(x_2089, 1, x_2087);
@ -33940,7 +33927,7 @@ lean_inc(x_45);
lean_dec(x_43);
x_46 = l_Array_empty___closed__1;
x_47 = lean_array_push(x_46, x_15);
x_48 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__34;
x_48 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__14;
x_49 = lean_array_push(x_47, x_48);
x_50 = l_Lean_Elab_Term_Do_ToCodeBlock_doForToCode___closed__4;
x_51 = l_Lean_addMacroScope(x_44, x_50, x_41);
@ -33954,7 +33941,7 @@ lean_ctor_set(x_56, 1, x_54);
lean_ctor_set(x_56, 2, x_51);
lean_ctor_set(x_56, 3, x_55);
x_57 = lean_array_push(x_49, x_56);
x_58 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__13;
x_58 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__9;
x_59 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_59, 0, x_58);
lean_ctor_set(x_59, 1, x_57);
@ -34251,7 +34238,7 @@ lean_inc(x_229);
lean_dec(x_227);
x_230 = l_Array_empty___closed__1;
x_231 = lean_array_push(x_230, x_15);
x_232 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__34;
x_232 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__14;
x_233 = lean_array_push(x_231, x_232);
x_234 = l_Lean_Elab_Term_Do_ToCodeBlock_doForToCode___closed__4;
lean_inc(x_225);
@ -34267,7 +34254,7 @@ lean_ctor_set(x_240, 1, x_238);
lean_ctor_set(x_240, 2, x_235);
lean_ctor_set(x_240, 3, x_239);
x_241 = lean_array_push(x_233, x_240);
x_242 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__13;
x_242 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__9;
x_243 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_243, 0, x_242);
lean_ctor_set(x_243, 1, x_241);
@ -34401,7 +34388,7 @@ x_321 = lean_array_push(x_320, x_301);
x_322 = l_Array_myMacro____x40_Init_Data_Array_Macros___hyg_464____closed__14;
x_323 = lean_array_push(x_321, x_322);
x_324 = lean_array_push(x_300, x_232);
x_325 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__38;
x_325 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__37;
lean_inc(x_324);
x_326 = lean_array_push(x_324, x_325);
x_327 = lean_alloc_ctor(1, 2, 0);
@ -34423,7 +34410,7 @@ x_336 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_336, 0, x_252);
lean_ctor_set(x_336, 1, x_335);
x_337 = lean_array_push(x_319, x_336);
x_338 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__46;
x_338 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__45;
x_339 = lean_array_push(x_324, x_338);
x_340 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_340, 0, x_242);
@ -34573,9 +34560,9 @@ x_419 = lean_array_push(x_230, x_418);
x_420 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_420, 0, x_252);
lean_ctor_set(x_420, 1, x_419);
x_421 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42;
x_421 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__41;
x_422 = lean_array_push(x_421, x_420);
x_423 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40;
x_423 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39;
x_424 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_424, 0, x_423);
lean_ctor_set(x_424, 1, x_422);
@ -38532,7 +38519,7 @@ x_95 = lean_name_eq(x_69, x_94);
if (x_95 == 0)
{
lean_object* x_96; uint8_t x_97;
x_96 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40;
x_96 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39;
x_97 = lean_name_eq(x_69, x_96);
if (x_97 == 0)
{
@ -40391,7 +40378,7 @@ x_531 = lean_name_eq(x_505, x_530);
if (x_531 == 0)
{
lean_object* x_532; uint8_t x_533;
x_532 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__40;
x_532 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__39;
x_533 = lean_name_eq(x_505, x_532);
if (x_533 == 0)
{
@ -43542,8 +43529,6 @@ l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__47 = _init_l_Lean_Ela
lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__47);
l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__48 = _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__48();
lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__48);
l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49 = _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49();
lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49);
l_Array_forMAux___main___at_Lean_Elab_Term_Do_ToCodeBlock_checkReassignable___spec__2___closed__1 = _init_l_Array_forMAux___main___at_Lean_Elab_Term_Do_ToCodeBlock_checkReassignable___spec__2___closed__1();
lean_mark_persistent(l_Array_forMAux___main___at_Lean_Elab_Term_Do_ToCodeBlock_checkReassignable___spec__2___closed__1);
l_Array_forMAux___main___at_Lean_Elab_Term_Do_ToCodeBlock_checkReassignable___spec__2___closed__2 = _init_l_Array_forMAux___main___at_Lean_Elab_Term_Do_ToCodeBlock_checkReassignable___spec__2___closed__2();

11035
stage0/stdlib/Lean/Elab/Match.c generated
View file

File diff suppressed because it is too large Load diff

166
stage0/stdlib/Lean/Elab/StructInst.c generated
View file

@ -308,6 +308,7 @@ lean_object* lean_expr_dbg_to_string(lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_defaultMissing_x3f(lean_object*);
lean_object* l_Lean_getPathToBaseStructure_x3f(lean_object*, lean_object*, lean_object*);
lean_object* l_List_mapM___main___at___private_Lean_Elab_StructInst_9__expandNumLitFields___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Elab_App_22__elabAppFn___main___closed__9;
size_t lean_usize_modn(size_t, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_findDefaultMissing_x3f___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_isRoundDone___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -354,7 +355,6 @@ lean_object* l_List_map___main___at_Lean_Elab_Term_StructInst_formatStruct___mai
lean_object* l_Lean_mkAtomFrom(lean_object*, lean_object*);
size_t l_USize_mod(size_t, size_t);
lean_object* l_Lean_Elab_Term_StructInst_FieldLHS_inhabited;
lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__28;
lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__15;
lean_object* l___private_Lean_Elab_StructInst_9__expandNumLitFields___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ConstantInfo_lparams(lean_object*);
@ -384,7 +384,6 @@ lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_throwFailedToElabField___rarg___closed__4;
lean_object* l_Std_AssocList_find_x3f___main___at___private_Lean_Elab_StructInst_12__mkFieldMap___spec__2___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__22;
extern lean_object* l___private_Lean_Elab_App_22__elabAppFn___main___closed__13;
uint8_t l_Lean_Expr_isMVar(lean_object*);
lean_object* l_Array_foldlStepMAux___main___at___private_Lean_Elab_StructInst_3__isModifyOp_x3f___spec__1___closed__5;
lean_object* l_Lean_Elab_Term_StructInst_Struct_modifyFieldsM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -395,6 +394,7 @@ uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_List_foldr___main___at_Lean_Elab_Term_StructInst_Struct_allDefault___main___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
extern lean_object* l_Lean_SourceInfo_inhabited___closed__1;
extern lean_object* l___private_Lean_Elab_App_22__elabAppFn___main___closed__14;
lean_object* l_Lean_Elab_Term_StructInst_Struct_source___boxed(lean_object*);
lean_object* l_Lean_Expr_betaRev(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_formatField___closed__2;
@ -2204,31 +2204,19 @@ return x_3;
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_SourceInfo_inhabited___closed__1;
x_2 = l_System_FilePath_dirName___closed__1;
x_3 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__3;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__11() {
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__3;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__10;
x_3 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__9;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -2236,7 +2224,7 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__12() {
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__11() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -2246,7 +2234,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__13() {
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -2256,13 +2244,25 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__13() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__12;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__13;
x_3 = lean_alloc_ctor(0, 2, 0);
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
@ -2271,31 +2271,19 @@ return x_3;
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__15() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__14;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_App_19__elabAppLValsAux___main___closed__1;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__17() {
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___private_Lean_Elab_App_19__elabAppLValsAux___main___closed__1;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__16;
x_3 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__15;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -2303,7 +2291,7 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__18() {
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__17() {
_start:
{
lean_object* x_1;
@ -2311,12 +2299,22 @@ x_1 = lean_mk_string("\n===>\n");
return x_1;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__17;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__19() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__18;
x_2 = lean_alloc_ctor(2, 1, 0);
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
@ -2324,19 +2322,19 @@ return x_2;
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__20() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__19;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
lean_object* x_1;
x_1 = lean_mk_string("\nval: ");
return x_1;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__21() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("\nval: ");
return x_1;
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__20;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__22() {
@ -2344,7 +2342,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__21;
x_2 = lean_alloc_ctor(2, 1, 0);
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
@ -2352,11 +2350,13 @@ return x_2;
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__23() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__22;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__12;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__24() {
@ -2364,8 +2364,8 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__13;
x_3 = lean_alloc_ctor(0, 2, 0);
x_2 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__23;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
@ -2374,21 +2374,19 @@ return x_3;
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__25() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__24;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
lean_object* x_1;
x_1 = lean_mk_string("\nSource: ");
return x_1;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__26() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("\nSource: ");
return x_1;
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__25;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__27() {
@ -2396,16 +2394,6 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__26;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__28() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__27;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -2431,7 +2419,7 @@ lean_object* x_306; lean_object* x_307; lean_object* x_308; lean_object* x_309;
lean_inc(x_2);
x_306 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_306, 0, x_2);
x_307 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__28;
x_307 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__27;
x_308 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_308, 0, x_306);
lean_ctor_set(x_308, 1, x_307);
@ -2581,7 +2569,7 @@ lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_166;
lean_inc(x_1);
x_163 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_163, 0, x_1);
x_164 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__23;
x_164 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__22;
x_165 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_165, 0, x_163);
lean_ctor_set(x_165, 1, x_164);
@ -2621,21 +2609,21 @@ lean_inc(x_60);
lean_dec(x_58);
x_61 = l_Array_empty___closed__1;
x_62 = lean_array_push(x_61, x_54);
x_63 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__9;
x_63 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__14;
x_64 = lean_array_push(x_62, x_63);
x_65 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__12;
x_65 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__11;
lean_inc(x_56);
lean_inc(x_59);
x_66 = l_Lean_addMacroScope(x_59, x_65, x_56);
x_67 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__11;
x_68 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__15;
x_67 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__10;
x_68 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__14;
x_69 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_69, 0, x_25);
lean_ctor_set(x_69, 1, x_67);
lean_ctor_set(x_69, 2, x_66);
lean_ctor_set(x_69, 3, x_68);
x_70 = lean_array_push(x_64, x_69);
x_71 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__13;
x_71 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__9;
x_72 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_72, 0, x_71);
lean_ctor_set(x_72, 1, x_70);
@ -2644,7 +2632,7 @@ x_74 = l___private_Lean_Elab_App_19__elabAppLValsAux___main___closed__2;
lean_inc(x_56);
lean_inc(x_59);
x_75 = l_Lean_addMacroScope(x_59, x_74, x_56);
x_76 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__17;
x_76 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__16;
x_77 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_77, 0, x_25);
lean_ctor_set(x_77, 1, x_76);
@ -2774,7 +2762,7 @@ lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137;
lean_inc(x_1);
x_134 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_134, 0, x_1);
x_135 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__20;
x_135 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__19;
x_136 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_136, 0, x_134);
lean_ctor_set(x_136, 1, x_135);
@ -2881,23 +2869,23 @@ lean_inc(x_193);
lean_dec(x_191);
x_194 = l_Array_empty___closed__1;
x_195 = lean_array_push(x_194, x_187);
x_196 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__9;
x_196 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__14;
x_197 = lean_array_push(x_195, x_196);
x_198 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__12;
x_198 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__11;
lean_inc(x_189);
lean_inc(x_192);
x_199 = l_Lean_addMacroScope(x_192, x_198, x_189);
x_200 = lean_box(0);
x_201 = l_Lean_SourceInfo_inhabited___closed__1;
x_202 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__11;
x_203 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__25;
x_202 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__10;
x_203 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__24;
x_204 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_204, 0, x_201);
lean_ctor_set(x_204, 1, x_202);
lean_ctor_set(x_204, 2, x_199);
lean_ctor_set(x_204, 3, x_203);
x_205 = lean_array_push(x_197, x_204);
x_206 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__13;
x_206 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__9;
x_207 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_207, 0, x_206);
lean_ctor_set(x_207, 1, x_205);
@ -2906,7 +2894,7 @@ x_209 = l___private_Lean_Elab_App_19__elabAppLValsAux___main___closed__2;
lean_inc(x_189);
lean_inc(x_192);
x_210 = l_Lean_addMacroScope(x_192, x_209, x_189);
x_211 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__17;
x_211 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__16;
x_212 = lean_alloc_ctor(3, 4, 0);
lean_ctor_set(x_212, 0, x_201);
lean_ctor_set(x_212, 1, x_211);
@ -3043,7 +3031,7 @@ lean_object* x_274; lean_object* x_275; lean_object* x_276; lean_object* x_277;
lean_inc(x_1);
x_274 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_274, 0, x_1);
x_275 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__20;
x_275 = l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__19;
x_276 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_276, 0, x_274);
lean_ctor_set(x_276, 1, x_275);
@ -13859,7 +13847,7 @@ x_6 = l___private_Lean_Elab_Term_5__tryCoe___closed__3;
x_7 = lean_array_push(x_6, x_1);
x_8 = lean_array_push(x_7, x_4);
x_9 = lean_array_push(x_8, x_5);
x_10 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__13;
x_10 = l___private_Lean_Elab_App_22__elabAppFn___main___closed__9;
x_11 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_11, 1, x_9);
@ -28030,8 +28018,6 @@ l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__26 = _init_l___privat
lean_mark_persistent(l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__26);
l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__27 = _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__27();
lean_mark_persistent(l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__27);
l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__28 = _init_l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__28();
lean_mark_persistent(l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__28);
l___private_Lean_Elab_StructInst_5__getStructName___rarg___closed__1 = _init_l___private_Lean_Elab_StructInst_5__getStructName___rarg___closed__1();
lean_mark_persistent(l___private_Lean_Elab_StructInst_5__getStructName___rarg___closed__1);
l___private_Lean_Elab_StructInst_5__getStructName___rarg___closed__2 = _init_l___private_Lean_Elab_StructInst_5__getStructName___rarg___closed__2();

6
stage0/stdlib/Lean/Elab/Tactic/Match.c generated
View file

@ -36,6 +36,7 @@ lean_object* l_Array_mapSepElemsM___at___private_Lean_Elab_Tactic_Match_1__mkAux
lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getMainModule___rarg(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
extern lean_object* l___private_Lean_Elab_Match_40__elabMatchAux___closed__1;
lean_object* l___private_Lean_Elab_Tactic_Match_2__mkAuxiliaryMatchTerm___closed__1;
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalMatch___spec__1___rarg(lean_object*);
extern lean_object* l_Lean_Elab_Tactic_evalCase___closed__4;
@ -44,7 +45,6 @@ lean_object* lean_array_fget(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
extern lean_object* l___private_Lean_Elab_Match_38__elabMatchAux___closed__1;
lean_object* l_Lean_Name_appendIndexAfter(lean_object*, lean_object*);
extern lean_object* l___private_Lean_Elab_Binders_12__expandFunBindersAux___main___closed__2;
lean_object* l___private_Lean_Elab_Tactic_Match_1__mkAuxiliaryMatchTermAux___lambda__1___closed__3;
@ -334,7 +334,7 @@ if (x_47 == 0)
{
lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60;
x_48 = lean_ctor_get(x_3, 0);
x_49 = l___private_Lean_Elab_Match_38__elabMatchAux___closed__1;
x_49 = l___private_Lean_Elab_Match_40__elabMatchAux___closed__1;
lean_inc(x_48);
x_50 = l_Lean_Name_appendIndexAfter(x_49, x_48);
x_51 = l_Lean_Name_append___main(x_1, x_50);
@ -366,7 +366,7 @@ x_62 = lean_ctor_get(x_3, 1);
lean_inc(x_62);
lean_inc(x_61);
lean_dec(x_3);
x_63 = l___private_Lean_Elab_Match_38__elabMatchAux___closed__1;
x_63 = l___private_Lean_Elab_Match_40__elabMatchAux___closed__1;
lean_inc(x_61);
x_64 = l_Lean_Name_appendIndexAfter(x_63, x_61);
x_65 = l_Lean_Name_append___main(x_1, x_64);