chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
f220654a27
commit
b415648fff
6 changed files with 1646 additions and 964 deletions
48
stage0/src/Lean/Elab/SyntheticMVars.lean
generated
48
stage0/src/Lean/Elab/SyntheticMVars.lean
generated
|
|
@ -88,13 +88,6 @@ private def synthesizePendingCoeInstMVar
|
|||
| Exception.error _ msg => throwTypeMismatchError errorMsgHeader? expectedType eType e f? msg
|
||||
| _ => unreachable!
|
||||
|
||||
/--
|
||||
Return `true` iff `mvarId` is assigned to a term whose the
|
||||
head is not a metavariable. We use this method to process `SyntheticMVarKind.withDefault`. -/
|
||||
private def checkWithDefault (mvarId : MVarId) : TermElabM Bool := do
|
||||
let val ← instantiateMVars (mkMVar mvarId)
|
||||
pure $ !val.getAppFn.isMVar
|
||||
|
||||
/-- Try to synthesize the given pending synthetic metavariable. -/
|
||||
private def synthesizeSyntheticMVar (mvarSyntheticDecl : SyntheticMVarDecl) (postponeOnError : Bool) (runTactics : Bool) : TermElabM Bool :=
|
||||
withRef mvarSyntheticDecl.stx do
|
||||
|
|
@ -102,7 +95,6 @@ private def synthesizeSyntheticMVar (mvarSyntheticDecl : SyntheticMVarDecl) (pos
|
|||
| SyntheticMVarKind.typeClass => synthesizePendingInstMVar mvarSyntheticDecl.mvarId
|
||||
| SyntheticMVarKind.coe header? expectedType eType e f? => synthesizePendingCoeInstMVar mvarSyntheticDecl.mvarId header? expectedType eType e f?
|
||||
-- NOTE: actual processing at `synthesizeSyntheticMVarsAux`
|
||||
| SyntheticMVarKind.withDefault _ => checkWithDefault mvarSyntheticDecl.mvarId
|
||||
| SyntheticMVarKind.postponed macroStack declName? => resumePostponed macroStack declName? mvarSyntheticDecl.stx mvarSyntheticDecl.mvarId postponeOnError
|
||||
| SyntheticMVarKind.tactic declName? tacticCode =>
|
||||
withReader (fun ctx => { ctx with declName? := declName? }) do
|
||||
|
|
@ -142,19 +134,31 @@ private def synthesizeSyntheticMVarsStep (postponeOnError : Bool) (runTactics :
|
|||
Return true if something was synthesized. -/
|
||||
def synthesizeUsingDefault : TermElabM Bool := do
|
||||
let s ← get
|
||||
let len := s.syntheticMVars.length
|
||||
let newSyntheticMVars ← s.syntheticMVars.filterM fun mvarDecl =>
|
||||
withRef mvarDecl.stx $
|
||||
let currLength := s.syntheticMVars.length
|
||||
let mut syntheticMVarsNew := []
|
||||
/- Recall that s.syntheticMVars is essentially a stack. The first metavariable was the last one created.
|
||||
We want to apply the default instance in reverse creation order. Otherwise,
|
||||
`toString 0` will produce a `OfNat String` cannot be synthesized error. -/
|
||||
for mvarDecl in s.syntheticMVars.reverse do
|
||||
match mvarDecl.kind with
|
||||
| SyntheticMVarKind.withDefault defaultVal => withMVarContext mvarDecl.mvarId do
|
||||
let val ← instantiateMVars (mkMVar mvarDecl.mvarId)
|
||||
if val.getAppFn.isMVar && !(← isDefEq val defaultVal) then
|
||||
-- TODO: better error message
|
||||
throwError! "failed to assign default value to metavariable{indentExpr val}\ndefault value{indentExpr defaultVal}"
|
||||
pure false
|
||||
| _ => pure true
|
||||
modify fun s => { s with syntheticMVars := newSyntheticMVars }
|
||||
pure $ newSyntheticMVars.length != len
|
||||
| SyntheticMVarKind.typeClass =>
|
||||
syntheticMVarsNew ← withMVarContext mvarDecl.mvarId do
|
||||
let mvarType := (← getMVarDecl mvarDecl.mvarId).type
|
||||
match (← isClass? mvarType) with
|
||||
| none => return mvarDecl :: syntheticMVarsNew
|
||||
| some className => match (← getDefaultInstances className) with
|
||||
| [] => return mvarDecl :: syntheticMVarsNew
|
||||
| defaultInstances =>
|
||||
for defaultInstance in defaultInstances do
|
||||
let candidate := Lean.mkConst defaultInstance
|
||||
trace[Elab.resume]! "trying default instance for {mkMVar mvarDecl.mvarId} := {candidate}"
|
||||
if (← isDefEqGuarded (mkMVar mvarDecl.mvarId) candidate) then
|
||||
return syntheticMVarsNew
|
||||
return mvarDecl :: syntheticMVarsNew
|
||||
| _ => syntheticMVarsNew := mvarDecl :: syntheticMVarsNew
|
||||
pure ()
|
||||
modify fun s => { s with syntheticMVars := syntheticMVarsNew }
|
||||
return syntheticMVarsNew.length != currLength
|
||||
|
||||
/-- Report an error for each synthetic metavariable that could not be resolved. -/
|
||||
private def reportStuckSyntheticMVars : TermElabM Unit := do
|
||||
|
|
@ -183,14 +187,14 @@ private def getSomeSynthethicMVarsRef : TermElabM Syntax := do
|
|||
then `syntheticMVars` is `[]` after executing this method.
|
||||
|
||||
It keeps executing `synthesizeSyntheticMVarsStep` while progress is being made.
|
||||
If `mayPostpone == false`, then it applies default values to `SyntheticMVarKind.withDefault`
|
||||
If `mayPostpone == false`, then it applies default instances to `SyntheticMVarKind.typeClass` (if available)
|
||||
metavariables that are still unresolved, and then tries to resolve metavariables
|
||||
with `mayPostpone == false`. That is, we force them to produce error messages and/or commit to
|
||||
a "best option". If, after that, we still haven't made progress, we report "stuck" errors. -/
|
||||
partial def synthesizeSyntheticMVars (mayPostpone := true) : TermElabM Unit :=
|
||||
let rec loop (u : Unit) : TermElabM Unit := do
|
||||
let ref ← getSomeSynthethicMVarsRef
|
||||
withRef ref $ withIncRecDepth do
|
||||
withRef ref <| withIncRecDepth do
|
||||
let s ← get
|
||||
unless s.syntheticMVars.isEmpty do
|
||||
if ← synthesizeSyntheticMVarsStep false false then
|
||||
|
|
|
|||
3
stage0/src/Lean/Elab/Term.lean
generated
3
stage0/src/Lean/Elab/Term.lean
generated
|
|
@ -107,8 +107,6 @@ inductive SyntheticMVarKind :=
|
|||
| tactic (declName? : Option Name) (tacticCode : Syntax)
|
||||
-- `elabTerm` call that threw `Exception.postpone` (input is stored at `SyntheticMVarDecl.ref`)
|
||||
| postponed (macroStack : MacroStack) (declName? : Option Name)
|
||||
-- type defaulting (currently: defaulting numeric literals to `Nat`)
|
||||
| withDefault (defaultVal : Expr)
|
||||
|
||||
structure SyntheticMVarDecl :=
|
||||
(mvarId : MVarId) (stx : Syntax) (kind : SyntheticMVarKind)
|
||||
|
|
@ -1240,7 +1238,6 @@ def resolveName (n : Name) (preresolved : List (Name × List String)) (explicitL
|
|||
| some val => pure (mkNatLit val)
|
||||
| none => throwIllFormedSyntax
|
||||
let typeMVar ← mkFreshTypeMVar MetavarKind.synthetic
|
||||
registerSyntheticMVar stx typeMVar.mvarId! (SyntheticMVarKind.withDefault (Lean.mkConst `Nat))
|
||||
match expectedType? with
|
||||
| some expectedType => isDefEq expectedType typeMVar; pure ()
|
||||
| _ => pure ()
|
||||
|
|
|
|||
1
stage0/stdlib/Lean/Elab/Match.c
generated
1
stage0/stdlib/Lean/Elab/Match.c
generated
|
|
@ -24832,6 +24832,7 @@ x_36 = lean_ctor_get(x_35, 1);
|
|||
lean_inc(x_36);
|
||||
lean_dec(x_35);
|
||||
lean_inc(x_10);
|
||||
lean_inc(x_9);
|
||||
lean_inc(x_8);
|
||||
lean_inc(x_7);
|
||||
lean_inc(x_6);
|
||||
|
|
|
|||
2205
stage0/stdlib/Lean/Elab/SyntheticMVars.c
generated
2205
stage0/stdlib/Lean/Elab/SyntheticMVars.c
generated
File diff suppressed because it is too large
Load diff
32
stage0/stdlib/Lean/Elab/Tactic/Induction.c
generated
32
stage0/stdlib/Lean/Elab/Tactic/Induction.c
generated
|
|
@ -221,7 +221,6 @@ lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_
|
|||
lean_object* lean_array_fget(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_CoreM_0__Lean_Core_mkFreshNameImp(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_addNewArg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getAltNumFields___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_map___at_Lean_resolveGlobalConstNoOverload___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
|
||||
|
|
@ -376,7 +375,6 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_evalInduction___spec__
|
|||
extern lean_object* l_Lean_Elab_Tactic_tacticElabAttribute;
|
||||
lean_object* l_Lean_Elab_Tactic_ElimApp_evalAlts_match__6(lean_object*);
|
||||
lean_object* l_Lean_Meta_instantiateMVars___at_Lean_Elab_Tactic_evalInduction___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getAltNumFields___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_evalCasesUsing___spec__1(lean_object*, size_t, size_t, 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_ElimApp_mkElimApp_loop(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_evalCasesUsing___lambda__2(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*, lean_object*, lean_object*);
|
||||
|
|
@ -586,6 +584,7 @@ lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecIn
|
|||
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecInfo_match__3(lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecInfo___lambda__1(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_Induction_0__Lean_Elab_Tactic_ElimApp_getAltNumFields___lambda__1___closed__1;
|
||||
lean_object* l_List_forIn_loop___at_Lean_Elab_Term_synthesizeUsingDefault___spec__4___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_evalIntros___spec__1(size_t, size_t, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecInfo_match__4___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getRecInfo_match__1(lean_object*);
|
||||
|
|
@ -3685,18 +3684,6 @@ x_2 = lean_alloc_closure((void*)(l___private_Lean_Elab_Tactic_Induction_0__Lean_
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getAltNumFields___spec__1___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_10; lean_object* x_11;
|
||||
x_10 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_10, 0, x_1);
|
||||
x_11 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_11, 0, x_10);
|
||||
lean_ctor_set(x_11, 1, x_9);
|
||||
return x_11;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getAltNumFields___spec__1___closed__1() {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -3741,7 +3728,7 @@ if (x_18 == 0)
|
|||
lean_object* x_19; lean_object* x_20; lean_object* x_21;
|
||||
lean_dec(x_16);
|
||||
lean_inc(x_2);
|
||||
x_19 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getAltNumFields___spec__1___lambda__1___boxed), 9, 1);
|
||||
x_19 = lean_alloc_closure((void*)(l_List_forIn_loop___at_Lean_Elab_Term_synthesizeUsingDefault___spec__4___lambda__1___boxed), 9, 1);
|
||||
lean_closure_set(x_19, 0, x_2);
|
||||
x_20 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getAltNumFields___spec__1___closed__1;
|
||||
lean_inc(x_12);
|
||||
|
|
@ -4014,21 +4001,6 @@ return x_30;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getAltNumFields___spec__1___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_10;
|
||||
x_10 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getAltNumFields___spec__1___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
return x_10;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getAltNumFields___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* 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) {
|
||||
_start:
|
||||
{
|
||||
|
|
|
|||
321
stage0/stdlib/Lean/Elab/Term.c
generated
321
stage0/stdlib/Lean/Elab/Term.c
generated
|
|
@ -61,9 +61,11 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_isExplicitApp___boxed(
|
|||
lean_object* l___regBuiltin_Lean_Elab_Term_elabBadCDot___closed__2;
|
||||
lean_object* lean_erase_macro_scopes(lean_object*);
|
||||
lean_object* l_ReaderT_read___at_Lean_Elab_Term_instMonadLogTermElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__4;
|
||||
lean_object* l_Lean_Syntax_isNatLitAux(lean_object*, lean_object*);
|
||||
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1(lean_object*, lean_object*, uint8_t, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_stringToMessageData(lean_object*);
|
||||
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7334____closed__1;
|
||||
lean_object* l_Lean_Elab_Term_Context_levelNames___default;
|
||||
lean_object* l_Std_PersistentArray_forM___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_MessageData_isNest(lean_object*);
|
||||
|
|
@ -75,14 +77,13 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux___
|
|||
lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabSort___closed__2;
|
||||
lean_object* l_Lean_mkSort(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__4;
|
||||
lean_object* l_Lean_Elab_Term_elabEnsureTypeOf_match__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Std_RBNode_insert___at_Lean_NameSet_insert___spec__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_foldl___at_Lean_Elab_addMacroStack___spec__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_getLetRecsToLift___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_instMonadMacroAdapterTermElabM___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_instMonadResolveNameTermElabM___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabNumLit___lambda__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_Term_elabNumLit___lambda__1___boxed(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_withIncRecDepth___rarg___lambda__2___closed__2;
|
||||
extern lean_object* l_Lean_Meta_setInlineAttribute___rarg___closed__2;
|
||||
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe___closed__9;
|
||||
|
|
@ -129,21 +130,20 @@ lean_object* l_Lean_Elab_logTrace___at_Lean_Elab_Term_traceAtCmdPos___spec__1___
|
|||
lean_object* l_Lean_Elab_Term_instInhabitedTermElabM___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Elab_throwUnsupportedSyntax___rarg___closed__1;
|
||||
lean_object* l_Lean_getConstInfo___at_Lean_Elab_Term_mkConst___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__2;
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__1;
|
||||
lean_object* l_Lean_Elab_Term_resolveLocalName_loop___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar_match__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__3___closed__4;
|
||||
lean_object* l_Lean_Elab_Term_elabNumLit___lambda__2___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_instMonadResolveNameTermElabM___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_resolveLocalName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_instMonadMacroAdapterTermElabM___closed__6;
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabQuotedName___closed__1;
|
||||
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe_match__2(lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabEnsureTypeOf___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_elabNumLit___lambda__1(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_initFn____x40_Lean_Elab_Term___hyg_1059____closed__1;
|
||||
lean_object* l_Lean_Elab_Term_elabNumLit___lambda__1(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_Term_elabTypeStx___closed__3;
|
||||
lean_object* l_Lean_Meta_instantiateMVars___at_Lean_Elab_Term_MVarErrorInfo_logError___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__2;
|
||||
lean_object* l_Lean_Meta_getMVarsAtDeclImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_registerCustomErrorIfMVar_match__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__3___closed__1;
|
||||
|
|
@ -230,7 +230,6 @@ extern lean_object* l_Lean_Meta_decLevel___rarg___lambda__1___closed__4;
|
|||
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_expr_instantiate1(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_instToExprChar___lambda__1___closed__1;
|
||||
extern lean_object* l_Lean_Literal_type___closed__3;
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabBadCDot___closed__1;
|
||||
lean_object* lean_array_push(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_getMessageLog___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -401,7 +400,7 @@ lean_object* l_Lean_Elab_Term_getMessageLog(lean_object*);
|
|||
lean_object* l_Std_AssocList_find_x3f___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___spec__6(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_initFn____x40_Lean_Data_Options___hyg_476____closed__3;
|
||||
lean_object* l_Lean_Meta_mkFreshLevelMVar___at___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabNumLit___lambda__2(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_elabNumLit___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_st_ref_take(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_instToStringLVal_match__1(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_MVarErrorInfo_logError___closed__2;
|
||||
|
|
@ -460,6 +459,7 @@ lean_object* l_Lean_Meta_mkAppOptM___at___private_Lean_Elab_Term_0__Lean_Elab_Te
|
|||
lean_object* l_Lean_Elab_Term_elabQuotedName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_foldlM___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___spec__6___lambda__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*);
|
||||
lean_object* l_Lean_Meta_trySynthInstance___at_Lean_Elab_Term_synthesizeInstMVarCore___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5715____closed__1;
|
||||
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_liftAttrM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Meta_instMetaEvalMetaM___rarg___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_mkInstMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -491,9 +491,9 @@ lean_object* l_Lean_Elab_Term_elabCharLit_match__1___rarg(lean_object*, lean_obj
|
|||
lean_object* l_Lean_MessageLog_forM___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_instMonadResolveNameTermElabM___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_levelMVarToParam_x27___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_initFn____x40_Lean_Elab_Term___hyg_5716____closed__1;
|
||||
extern lean_object* l_Lean_KeyedDeclsAttribute_instInhabitedKeyedDeclsAttribute___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_instMonadMacroAdapterTermElabM___closed__8;
|
||||
lean_object* l_Lean_Elab_Term_elabNumLit___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_instMonadLiftTMetaMTermElabM(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_blockImplicitLambda___boxed(lean_object*);
|
||||
lean_object* l_Lean_Elab_throwUnboundImplicitLocal___at_Lean_Elab_Term_resolveName___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -541,12 +541,12 @@ lean_object* l_Lean_Elab_Term_mkTypeMismatchError_match__1___rarg(lean_object*,
|
|||
lean_object* l___regBuiltin_Lean_Elab_Term_elabCharLit(lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabOptLevel___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux_match__2___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5716_(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5715_(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_setElabConfig(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_getLetRecsToLift(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_liftLevelM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059_(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_802_(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058_(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_801_(lean_object*);
|
||||
extern lean_object* l_Lean_MessageData_nil___closed__1;
|
||||
lean_object* l_Std_PersistentArray_forMAux___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getId(lean_object*);
|
||||
|
|
@ -854,7 +854,6 @@ lean_object* l_Lean_Elab_Term_elabSort(lean_object*, lean_object*, lean_object*,
|
|||
uint8_t l_Lean_Elab_Term_levelMVarToParam___lambda__1(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe_match__2___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabSyntheticHole___closed__2;
|
||||
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7349____closed__1;
|
||||
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore_match__2(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_mkTypeMismatchError___closed__2;
|
||||
|
|
@ -982,7 +981,7 @@ lean_object* l_Lean_Elab_Term_logUnassignedUsingErrorInfos_match__2___rarg(lean_
|
|||
lean_object* l_Lean_Elab_Term_throwErrorIfErrors(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Meta_isLevelDefEq___rarg___lambda__2___closed__4;
|
||||
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7349_(lean_object*);
|
||||
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7334_(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabByTactic_match__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__2;
|
||||
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_instMetaEvalTermElabM___spec__5(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -1030,7 +1029,6 @@ lean_object* l_Lean_Elab_Term_registerCustomErrorIfMVar_match__1(lean_object*);
|
|||
uint8_t l___private_Lean_Elab_Term_0__Lean_Elab_Term_isExplicitApp(lean_object*);
|
||||
lean_object* l_Lean_Meta_setMCtx___at_Lean_Elab_Term_savingMCtx___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__3;
|
||||
lean_object* l_Array_contains___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___spec__2___boxed(lean_object*, lean_object*);
|
||||
uint8_t l_List_isEmpty___rarg(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_instInhabitedSavedState;
|
||||
|
|
@ -1052,6 +1050,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_elabSyntheticHole___closed__2;
|
|||
lean_object* l_Lean_Elab_Term_setMessageLog(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabTypeWithUnboundImplicit(lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoeSort___closed__4;
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__3;
|
||||
lean_object* l_Lean_Message_toString(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_mkAuxName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkAppB(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -2418,7 +2417,7 @@ _start:
|
|||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
||||
x_1 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__2;
|
||||
x_2 = l_Lean_Elab_Term_getFVarLocalDecl_x21___closed__3;
|
||||
x_3 = lean_unsigned_to_nat(225u);
|
||||
x_3 = lean_unsigned_to_nat(223u);
|
||||
x_4 = lean_unsigned_to_nat(14u);
|
||||
x_5 = l_Lean_Syntax_strLitToAtom___closed__3;
|
||||
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
|
||||
|
|
@ -3615,7 +3614,7 @@ lean_ctor_set(x_3, 1, x_1);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_802_(lean_object* x_1) {
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_801_(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
|
|
@ -4302,7 +4301,7 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_withoutErrToSorry___rarg), 8,
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__1() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -4310,17 +4309,17 @@ x_1 = lean_mk_string("unboundImplicitLocal");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__2() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__1;
|
||||
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__3() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -4328,13 +4327,13 @@ x_1 = lean_mk_string("Unbound local variables in declaration headers become impl
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__4() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_Lean_initFn____x40_Lean_Data_Options___hyg_476____closed__3;
|
||||
x_2 = l_Lean_instInhabitedParserDescr___closed__1;
|
||||
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__3;
|
||||
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__3;
|
||||
x_4 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_4, 0, x_1);
|
||||
lean_ctor_set(x_4, 1, x_2);
|
||||
|
|
@ -4342,12 +4341,12 @@ lean_ctor_set(x_4, 2, x_3);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059_(lean_object* x_1) {
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058_(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__2;
|
||||
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__4;
|
||||
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__2;
|
||||
x_3 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__4;
|
||||
x_4 = lean_register_option(x_2, x_3, x_1);
|
||||
return x_4;
|
||||
}
|
||||
|
|
@ -4356,7 +4355,7 @@ uint8_t l___private_Lean_Elab_Term_0__Lean_Elab_Term_getUnboundImplicitLocalOpti
|
|||
_start:
|
||||
{
|
||||
lean_object* x_2; uint8_t x_3; uint8_t x_4;
|
||||
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__2;
|
||||
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__2;
|
||||
x_3 = 1;
|
||||
x_4 = l_Lean_KVMap_getBool(x_1, x_2, x_3);
|
||||
return x_4;
|
||||
|
|
@ -29533,7 +29532,7 @@ lean_dec(x_3);
|
|||
return x_9;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5716____closed__1() {
|
||||
static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5715____closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
|
|
@ -29543,11 +29542,11 @@ x_3 = lean_name_mk_string(x_1, x_2);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5716_(lean_object* x_1) {
|
||||
lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5715_(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3;
|
||||
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5716____closed__1;
|
||||
x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5715____closed__1;
|
||||
x_3 = l_Lean_registerTraceClass(x_2, x_1);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -29714,7 +29713,7 @@ lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean
|
|||
x_89 = lean_ctor_get(x_83, 1);
|
||||
lean_inc(x_89);
|
||||
lean_dec(x_83);
|
||||
x_90 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5716____closed__1;
|
||||
x_90 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5715____closed__1;
|
||||
x_91 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(x_90, x_2, x_3, x_4, x_5, x_6, x_7, x_89);
|
||||
x_92 = lean_ctor_get(x_91, 0);
|
||||
lean_inc(x_92);
|
||||
|
|
@ -29756,7 +29755,7 @@ lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean
|
|||
x_49 = lean_ctor_get(x_43, 1);
|
||||
lean_inc(x_49);
|
||||
lean_dec(x_43);
|
||||
x_50 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5716____closed__1;
|
||||
x_50 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5715____closed__1;
|
||||
x_51 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(x_50, x_2, x_3, x_4, x_5, x_6, x_7, x_49);
|
||||
x_52 = lean_ctor_get(x_51, 0);
|
||||
lean_inc(x_52);
|
||||
|
|
@ -29833,7 +29832,7 @@ x_37 = l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__
|
|||
x_38 = lean_alloc_ctor(10, 2, 0);
|
||||
lean_ctor_set(x_38, 0, x_36);
|
||||
lean_ctor_set(x_38, 1, x_37);
|
||||
x_39 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5716____closed__1;
|
||||
x_39 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5715____closed__1;
|
||||
x_40 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_39, x_38, x_2, x_3, x_4, x_5, x_6, x_7, x_32);
|
||||
x_41 = lean_ctor_get(x_40, 1);
|
||||
lean_inc(x_41);
|
||||
|
|
@ -29891,7 +29890,7 @@ x_73 = l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__
|
|||
x_74 = lean_alloc_ctor(10, 2, 0);
|
||||
lean_ctor_set(x_74, 0, x_72);
|
||||
lean_ctor_set(x_74, 1, x_73);
|
||||
x_75 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5716____closed__1;
|
||||
x_75 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5715____closed__1;
|
||||
x_76 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_75, x_74, x_2, x_3, x_4, x_5, x_6, x_7, x_57);
|
||||
x_77 = lean_ctor_get(x_76, 1);
|
||||
lean_inc(x_77);
|
||||
|
|
@ -35455,42 +35454,43 @@ return x_369;
|
|||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Term_elabNumLit___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
|
||||
lean_object* l_Lean_Elab_Term_elabNumLit___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_12;
|
||||
lean_inc(x_10);
|
||||
lean_object* x_11;
|
||||
lean_inc(x_9);
|
||||
lean_inc(x_8);
|
||||
lean_inc(x_7);
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_1);
|
||||
x_12 = l___private_Lean_Meta_InferType_0__Lean_Meta_getLevelImp(x_1, x_7, x_8, x_9, x_10, x_11);
|
||||
if (lean_obj_tag(x_12) == 0)
|
||||
x_11 = l___private_Lean_Meta_InferType_0__Lean_Meta_getLevelImp(x_1, x_6, x_7, x_8, x_9, x_10);
|
||||
if (lean_obj_tag(x_11) == 0)
|
||||
{
|
||||
lean_object* x_13; lean_object* x_14; lean_object* x_15;
|
||||
x_13 = lean_ctor_get(x_12, 0);
|
||||
lean_object* x_12; lean_object* x_13; lean_object* x_14;
|
||||
x_12 = lean_ctor_get(x_11, 0);
|
||||
lean_inc(x_12);
|
||||
x_13 = lean_ctor_get(x_11, 1);
|
||||
lean_inc(x_13);
|
||||
x_14 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_14);
|
||||
lean_dec(x_12);
|
||||
x_15 = l_Lean_Meta_decLevel___at_Lean_Elab_Term_elabNumLit___spec__2(x_13, x_5, x_6, x_7, x_8, x_9, x_10, x_14);
|
||||
if (lean_obj_tag(x_15) == 0)
|
||||
lean_dec(x_11);
|
||||
x_14 = l_Lean_Meta_decLevel___at_Lean_Elab_Term_elabNumLit___spec__2(x_12, x_4, x_5, x_6, x_7, x_8, x_9, x_13);
|
||||
if (lean_obj_tag(x_14) == 0)
|
||||
{
|
||||
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;
|
||||
x_16 = lean_ctor_get(x_15, 0);
|
||||
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;
|
||||
x_15 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_15);
|
||||
x_16 = lean_ctor_get(x_14, 1);
|
||||
lean_inc(x_16);
|
||||
x_17 = lean_ctor_get(x_15, 1);
|
||||
lean_inc(x_17);
|
||||
lean_dec(x_15);
|
||||
lean_dec(x_14);
|
||||
x_17 = lean_box(0);
|
||||
x_18 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_18, 0, x_16);
|
||||
lean_ctor_set(x_18, 1, x_2);
|
||||
lean_ctor_set(x_18, 0, x_15);
|
||||
lean_ctor_set(x_18, 1, x_17);
|
||||
x_19 = l_Lean_Meta_evalNat___closed__2;
|
||||
lean_inc(x_18);
|
||||
x_20 = l_Lean_mkConst(x_19, x_18);
|
||||
lean_inc(x_1);
|
||||
x_21 = l_Lean_mkApp(x_20, x_1);
|
||||
x_22 = l_Lean_Elab_Term_mkInstMVar(x_21, x_5, x_6, x_7, x_8, x_9, x_10, x_17);
|
||||
x_22 = l_Lean_Elab_Term_mkInstMVar(x_21, x_4, x_5, x_6, x_7, x_8, x_9, x_16);
|
||||
if (lean_obj_tag(x_22) == 0)
|
||||
{
|
||||
uint8_t x_23;
|
||||
|
|
@ -35501,7 +35501,7 @@ lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
|
|||
x_24 = lean_ctor_get(x_22, 0);
|
||||
x_25 = l_Lean_Meta_evalNat___closed__3;
|
||||
x_26 = l_Lean_mkConst(x_25, x_18);
|
||||
x_27 = l_Lean_mkApp3(x_26, x_1, x_24, x_3);
|
||||
x_27 = l_Lean_mkApp3(x_26, x_1, x_24, x_2);
|
||||
lean_ctor_set(x_22, 0, x_27);
|
||||
return x_22;
|
||||
}
|
||||
|
|
@ -35515,7 +35515,7 @@ lean_inc(x_28);
|
|||
lean_dec(x_22);
|
||||
x_30 = l_Lean_Meta_evalNat___closed__3;
|
||||
x_31 = l_Lean_mkConst(x_30, x_18);
|
||||
x_32 = l_Lean_mkApp3(x_31, x_1, x_28, x_3);
|
||||
x_32 = l_Lean_mkApp3(x_31, x_1, x_28, x_2);
|
||||
x_33 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_33, 0, x_32);
|
||||
lean_ctor_set(x_33, 1, x_29);
|
||||
|
|
@ -35526,7 +35526,7 @@ else
|
|||
{
|
||||
uint8_t x_34;
|
||||
lean_dec(x_18);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_34 = !lean_is_exclusive(x_22);
|
||||
if (x_34 == 0)
|
||||
|
|
@ -35551,28 +35551,27 @@ return x_37;
|
|||
else
|
||||
{
|
||||
uint8_t x_38;
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_9);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_38 = !lean_is_exclusive(x_15);
|
||||
x_38 = !lean_is_exclusive(x_14);
|
||||
if (x_38 == 0)
|
||||
{
|
||||
return x_15;
|
||||
return x_14;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_39; lean_object* x_40; lean_object* x_41;
|
||||
x_39 = lean_ctor_get(x_15, 0);
|
||||
x_40 = lean_ctor_get(x_15, 1);
|
||||
x_39 = lean_ctor_get(x_14, 0);
|
||||
x_40 = lean_ctor_get(x_14, 1);
|
||||
lean_inc(x_40);
|
||||
lean_inc(x_39);
|
||||
lean_dec(x_15);
|
||||
lean_dec(x_14);
|
||||
x_41 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_41, 0, x_39);
|
||||
lean_ctor_set(x_41, 1, x_40);
|
||||
|
|
@ -35583,28 +35582,27 @@ return x_41;
|
|||
else
|
||||
{
|
||||
uint8_t x_42;
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_9);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_3);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_42 = !lean_is_exclusive(x_12);
|
||||
x_42 = !lean_is_exclusive(x_11);
|
||||
if (x_42 == 0)
|
||||
{
|
||||
return x_12;
|
||||
return x_11;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_43; lean_object* x_44; lean_object* x_45;
|
||||
x_43 = lean_ctor_get(x_12, 0);
|
||||
x_44 = lean_ctor_get(x_12, 1);
|
||||
x_43 = lean_ctor_get(x_11, 0);
|
||||
x_44 = lean_ctor_get(x_11, 1);
|
||||
lean_inc(x_44);
|
||||
lean_inc(x_43);
|
||||
lean_dec(x_12);
|
||||
lean_dec(x_11);
|
||||
x_45 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_45, 0, x_43);
|
||||
lean_ctor_set(x_45, 1, x_44);
|
||||
|
|
@ -35613,96 +35611,81 @@ return x_45;
|
|||
}
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_elabNumLit___lambda__2___closed__1() {
|
||||
lean_object* l_Lean_Elab_Term_elabNumLit___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Literal_type___closed__3;
|
||||
x_2 = lean_alloc_ctor(4, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Term_elabNumLit___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
|
||||
_start:
|
||||
uint8_t x_10; lean_object* x_11; lean_object* x_12;
|
||||
x_10 = 1;
|
||||
x_11 = lean_box(0);
|
||||
lean_inc(x_5);
|
||||
x_12 = l_Lean_Meta_mkFreshTypeMVar___at_Lean_Elab_Term_elabNumLit___spec__1(x_10, x_11, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
|
||||
if (lean_obj_tag(x_1) == 0)
|
||||
{
|
||||
uint8_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
|
||||
x_11 = 1;
|
||||
x_12 = lean_box(0);
|
||||
lean_inc(x_6);
|
||||
x_13 = l_Lean_Meta_mkFreshTypeMVar___at_Lean_Elab_Term_elabNumLit___spec__1(x_11, x_12, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
|
||||
x_14 = lean_ctor_get(x_13, 0);
|
||||
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
|
||||
x_13 = lean_ctor_get(x_12, 0);
|
||||
lean_inc(x_13);
|
||||
x_14 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_14);
|
||||
x_15 = lean_ctor_get(x_13, 1);
|
||||
lean_inc(x_15);
|
||||
lean_dec(x_13);
|
||||
x_16 = l_Lean_Expr_mvarId_x21(x_14);
|
||||
x_17 = lean_box(0);
|
||||
x_18 = l_Lean_Elab_Term_elabNumLit___lambda__2___closed__1;
|
||||
x_19 = l_Lean_Elab_Term_registerSyntheticMVar(x_1, x_16, x_18, x_4, x_5, x_6, x_7, x_8, x_9, x_15);
|
||||
if (lean_obj_tag(x_2) == 0)
|
||||
{
|
||||
lean_object* x_20; lean_object* x_21; lean_object* x_22;
|
||||
x_20 = lean_ctor_get(x_19, 1);
|
||||
lean_inc(x_20);
|
||||
lean_dec(x_19);
|
||||
x_21 = lean_box(0);
|
||||
x_22 = l_Lean_Elab_Term_elabNumLit___lambda__1(x_14, x_17, x_3, x_21, x_4, x_5, x_6, x_7, x_8, x_9, x_20);
|
||||
return x_22;
|
||||
lean_dec(x_12);
|
||||
x_15 = lean_box(0);
|
||||
x_16 = l_Lean_Elab_Term_elabNumLit___lambda__1(x_13, x_2, x_15, x_3, x_4, x_5, x_6, x_7, x_8, x_14);
|
||||
return x_16;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_23; lean_object* x_24; lean_object* x_25;
|
||||
x_23 = lean_ctor_get(x_19, 1);
|
||||
lean_inc(x_23);
|
||||
lean_dec(x_19);
|
||||
x_24 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_24);
|
||||
lean_dec(x_2);
|
||||
lean_inc(x_9);
|
||||
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
|
||||
x_17 = lean_ctor_get(x_12, 0);
|
||||
lean_inc(x_17);
|
||||
x_18 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_18);
|
||||
lean_dec(x_12);
|
||||
x_19 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_19);
|
||||
lean_dec(x_1);
|
||||
lean_inc(x_8);
|
||||
lean_inc(x_7);
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_14);
|
||||
x_25 = l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_elabNumLit___spec__3(x_24, x_14, x_4, x_5, x_6, x_7, x_8, x_9, x_23);
|
||||
if (lean_obj_tag(x_25) == 0)
|
||||
lean_inc(x_5);
|
||||
lean_inc(x_17);
|
||||
x_20 = l_Lean_Meta_isExprDefEq___at_Lean_Elab_Term_elabNumLit___spec__3(x_19, x_17, x_3, x_4, x_5, x_6, x_7, x_8, x_18);
|
||||
if (lean_obj_tag(x_20) == 0)
|
||||
{
|
||||
lean_object* x_26; lean_object* x_27; lean_object* x_28;
|
||||
x_26 = lean_ctor_get(x_25, 1);
|
||||
lean_inc(x_26);
|
||||
lean_dec(x_25);
|
||||
x_27 = lean_box(0);
|
||||
x_28 = l_Lean_Elab_Term_elabNumLit___lambda__1(x_14, x_17, x_3, x_27, x_4, x_5, x_6, x_7, x_8, x_9, x_26);
|
||||
return x_28;
|
||||
lean_object* x_21; lean_object* x_22; lean_object* x_23;
|
||||
x_21 = lean_ctor_get(x_20, 1);
|
||||
lean_inc(x_21);
|
||||
lean_dec(x_20);
|
||||
x_22 = lean_box(0);
|
||||
x_23 = l_Lean_Elab_Term_elabNumLit___lambda__1(x_17, x_2, x_22, x_3, x_4, x_5, x_6, x_7, x_8, x_21);
|
||||
return x_23;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_29;
|
||||
lean_dec(x_14);
|
||||
lean_dec(x_9);
|
||||
uint8_t x_24;
|
||||
lean_dec(x_17);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
x_29 = !lean_is_exclusive(x_25);
|
||||
if (x_29 == 0)
|
||||
lean_dec(x_2);
|
||||
x_24 = !lean_is_exclusive(x_20);
|
||||
if (x_24 == 0)
|
||||
{
|
||||
return x_25;
|
||||
return x_20;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_30; lean_object* x_31; lean_object* x_32;
|
||||
x_30 = lean_ctor_get(x_25, 0);
|
||||
x_31 = lean_ctor_get(x_25, 1);
|
||||
lean_inc(x_31);
|
||||
lean_inc(x_30);
|
||||
lean_dec(x_25);
|
||||
x_32 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_32, 0, x_30);
|
||||
lean_ctor_set(x_32, 1, x_31);
|
||||
return x_32;
|
||||
lean_object* x_25; lean_object* x_26; lean_object* x_27;
|
||||
x_25 = lean_ctor_get(x_20, 0);
|
||||
x_26 = lean_ctor_get(x_20, 1);
|
||||
lean_inc(x_26);
|
||||
lean_inc(x_25);
|
||||
lean_dec(x_20);
|
||||
x_27 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_27, 0, x_25);
|
||||
lean_ctor_set(x_27, 1, x_26);
|
||||
return x_27;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -35718,7 +35701,6 @@ if (lean_obj_tag(x_11) == 0)
|
|||
{
|
||||
lean_object* x_12; uint8_t x_13;
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
x_12 = l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Term_elabStrLit___spec__1(x_3, x_4, x_5, x_6, x_7, x_8, x_9);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
|
|
@ -35751,7 +35733,7 @@ x_17 = lean_ctor_get(x_11, 0);
|
|||
lean_inc(x_17);
|
||||
lean_dec(x_11);
|
||||
x_18 = l_Lean_mkNatLit(x_17);
|
||||
x_19 = l_Lean_Elab_Term_elabNumLit___lambda__2(x_1, x_2, x_18, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
|
||||
x_19 = l_Lean_Elab_Term_elabNumLit___lambda__2(x_2, x_18, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
|
||||
return x_19;
|
||||
}
|
||||
}
|
||||
|
|
@ -35815,20 +35797,29 @@ lean_dec(x_3);
|
|||
return x_10;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Term_elabNumLit___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
|
||||
lean_object* l_Lean_Elab_Term_elabNumLit___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_12;
|
||||
x_12 = l_Lean_Elab_Term_elabNumLit___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
|
||||
lean_dec(x_4);
|
||||
return x_12;
|
||||
lean_object* x_11;
|
||||
x_11 = l_Lean_Elab_Term_elabNumLit___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
|
||||
lean_dec(x_3);
|
||||
return x_11;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Term_elabNumLit___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_10;
|
||||
x_10 = l_Lean_Elab_Term_elabNumLit(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
|
||||
lean_dec(x_1);
|
||||
return x_10;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabNumLit___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabNumLit), 9, 0);
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabNumLit___boxed), 9, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
|
|
@ -39194,7 +39185,7 @@ x_8 = l_Lean_Elab_Term_instMetaEvalTermElabM___rarg(x_1, x_2, x_3, x_4, x_7, x_6
|
|||
return x_8;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7349____closed__1() {
|
||||
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7334____closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
|
|
@ -39204,7 +39195,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7349_(lean_object* x_1) {
|
||||
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7334_(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3;
|
||||
|
|
@ -39216,7 +39207,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
|||
x_4 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_4);
|
||||
lean_dec(x_3);
|
||||
x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7349____closed__1;
|
||||
x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7334____closed__1;
|
||||
x_6 = l_Lean_registerTraceClass(x_5, x_4);
|
||||
if (lean_obj_tag(x_6) == 0)
|
||||
{
|
||||
|
|
@ -39435,7 +39426,7 @@ l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__8 = _init_l_Lean_Elab_Term_
|
|||
lean_mark_persistent(l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__8);
|
||||
l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__9 = _init_l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__9();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__9);
|
||||
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_802_(lean_io_mk_world());
|
||||
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_801_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
l_Lean_Elab_Term_termElabAttribute = lean_io_result_get_value(res);
|
||||
lean_mark_persistent(l_Lean_Elab_Term_termElabAttribute);
|
||||
|
|
@ -39452,15 +39443,15 @@ l_Lean_Elab_Term_instMonadResolveNameTermElabM___closed__5 = _init_l_Lean_Elab_T
|
|||
lean_mark_persistent(l_Lean_Elab_Term_instMonadResolveNameTermElabM___closed__5);
|
||||
l_Lean_Elab_Term_instMonadResolveNameTermElabM = _init_l_Lean_Elab_Term_instMonadResolveNameTermElabM();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_instMonadResolveNameTermElabM);
|
||||
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__1);
|
||||
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__2();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__2);
|
||||
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__3 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__3);
|
||||
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__4 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__4();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059____closed__4);
|
||||
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1059_(lean_io_mk_world());
|
||||
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__1);
|
||||
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__2();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__2);
|
||||
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__3 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__3);
|
||||
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__4 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__4();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058____closed__4);
|
||||
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_1058_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Elab_Term_throwErrorIfErrors___closed__1 = _init_l_Lean_Elab_Term_throwErrorIfErrors___closed__1();
|
||||
|
|
@ -39671,9 +39662,9 @@ l_Lean_Elab_Term_mkAuxName___closed__2 = _init_l_Lean_Elab_Term_mkAuxName___clos
|
|||
lean_mark_persistent(l_Lean_Elab_Term_mkAuxName___closed__2);
|
||||
l_Lean_Elab_Term_mkAuxName___closed__3 = _init_l_Lean_Elab_Term_mkAuxName___closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_mkAuxName___closed__3);
|
||||
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5716____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5716____closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5716____closed__1);
|
||||
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5716_(lean_io_mk_world());
|
||||
l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5715____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5715____closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5715____closed__1);
|
||||
res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5715_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Elab_Term_isLetRecAuxMVar___closed__1 = _init_l_Lean_Elab_Term_isLetRecAuxMVar___closed__1();
|
||||
|
|
@ -39794,8 +39785,6 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabStrLit___closed__1);
|
|||
res = l___regBuiltin_Lean_Elab_Term_elabStrLit(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Elab_Term_elabNumLit___lambda__2___closed__1 = _init_l_Lean_Elab_Term_elabNumLit___lambda__2___closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_elabNumLit___lambda__2___closed__1);
|
||||
l___regBuiltin_Lean_Elab_Term_elabNumLit___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabNumLit___closed__1();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabNumLit___closed__1);
|
||||
res = l___regBuiltin_Lean_Elab_Term_elabNumLit(lean_io_mk_world());
|
||||
|
|
@ -39854,9 +39843,9 @@ l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__2 = _init_l_Lean_Elab_Te
|
|||
lean_mark_persistent(l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__2);
|
||||
l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3 = _init_l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__3);
|
||||
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7349____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7349____closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7349____closed__1);
|
||||
res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7349_(lean_io_mk_world());
|
||||
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7334____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7334____closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7334____closed__1);
|
||||
res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7334_(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
return lean_io_result_mk_ok(lean_box(0));
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue