chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
e9d85f49e6
commit
00f59a91ee
3 changed files with 2822 additions and 4235 deletions
62
stage0/src/Lean/Elab/Term.lean
generated
62
stage0/src/Lean/Elab/Term.lean
generated
|
|
@ -742,43 +742,6 @@ def isMonadApp (type : Expr) : TermElabM Bool := do
|
|||
let some (m, _) ← isTypeApp? type | pure false
|
||||
return (← isMonad? m) |>.isSome
|
||||
|
||||
/--
|
||||
Try to coerce `a : α` into `m β` by first coercing `a : α` into ‵β`, and then using `pure`.
|
||||
The method is only applied if `α` is not monadic (e.g., `Nat → IO Unit`), and the head symbol
|
||||
of the resulting type is not a metavariable (e.g., `?m Unit` or `Bool → ?m Nat`).
|
||||
|
||||
The main limitation of the approach above is polymorphic code. As usual, coercions and polymorphism
|
||||
do not interact well. In the example above, the lift is successfully applied to `true`, `false` and `!y`
|
||||
since none of them is polymorphic
|
||||
```
|
||||
def f (x : Bool) : IO Bool := do
|
||||
let y ← if x == 0 then IO.println "hello"; true else false;
|
||||
!y
|
||||
```
|
||||
On the other hand, the following fails since `+` is polymorphic
|
||||
```
|
||||
def f (x : Bool) : IO Nat := do
|
||||
IO.prinln x
|
||||
x + x -- Error: failed to synthesize `Add (IO Nat)`
|
||||
```
|
||||
-/
|
||||
private def tryPureCoe? (errorMsgHeader? : Option String) (m β α a : Expr) : TermElabM (Option Expr) :=
|
||||
commitWhenSome? do
|
||||
let doIt : TermElabM (Option Expr) := do
|
||||
try
|
||||
let aNew ← tryCoe errorMsgHeader? β α a none
|
||||
let aNew ← mkPure m aNew
|
||||
pure (some aNew)
|
||||
catch _ =>
|
||||
pure none
|
||||
forallTelescope α fun _ α => do
|
||||
if (← isMonadApp α) then
|
||||
pure none
|
||||
else if !α.getAppFn.isMVar then
|
||||
doIt
|
||||
else
|
||||
pure none
|
||||
|
||||
/-
|
||||
Try coercions and monad lifts to make sure `e` has type `expectedType`.
|
||||
|
||||
|
|
@ -787,13 +750,6 @@ Otherwise, we just use the basic `tryCoe`.
|
|||
|
||||
Extensions for monads.
|
||||
|
||||
Given an expected type of the form `n β`, if `eType` is of the form `α`, but not `m α`
|
||||
|
||||
1 - Try to coerce ‵α` into ‵β`, and use `pure` to lift it to `n α`.
|
||||
It only works if `n` implements `Pure`
|
||||
|
||||
If `eType` is of the form `m α`. We use the following approaches.
|
||||
|
||||
1- Try to unify `n` and `m`. If it succeeds, then we use
|
||||
```
|
||||
coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β
|
||||
|
|
@ -853,14 +809,7 @@ private def tryLiftAndCoe (errorMsgHeader? : Option String) (expectedType : Expr
|
|||
let tryCoeSimple : TermElabM Expr :=
|
||||
tryCoe errorMsgHeader? expectedType eType e f?
|
||||
let some (n, β) ← isTypeApp? expectedType | tryCoeSimple
|
||||
let tryPureCoeAndSimple : TermElabM Expr := do
|
||||
if autoLift.get (← getOptions) then
|
||||
match (← tryPureCoe? errorMsgHeader? n β eType e) with
|
||||
| some eNew => pure eNew
|
||||
| none => tryCoeSimple
|
||||
else
|
||||
tryCoeSimple
|
||||
let some (m, α) ← isTypeApp? eType | tryPureCoeAndSimple
|
||||
let some (m, α) ← isTypeApp? eType | tryCoeSimple
|
||||
if (← isDefEq m n) then
|
||||
let some monadInst ← isMonad? n | tryCoeSimple
|
||||
try expandCoe (← mkAppOptM ``Lean.Internal.coeM #[m, α, β, none, monadInst, e]) catch _ => throwMismatch
|
||||
|
|
@ -887,13 +836,8 @@ private def tryLiftAndCoe (errorMsgHeader? : Option String) (expectedType : Expr
|
|||
unless (← isDefEq expectedType eNewType) do throwMismatch
|
||||
return eNew -- approach 3 worked
|
||||
catch _ =>
|
||||
/-
|
||||
If `m` is not a monad, then we try to use `tryPureCoe?` and then `tryCoe?`.
|
||||
Otherwise, we just try `tryCoe?`.
|
||||
-/
|
||||
match (← isMonad? m) with
|
||||
| none => tryPureCoeAndSimple
|
||||
| some _ => tryCoeSimple
|
||||
/- If `m` is not a monad, then we try to use `tryCoe?`. -/
|
||||
tryCoeSimple
|
||||
else
|
||||
tryCoeSimple
|
||||
|
||||
|
|
|
|||
252
stage0/stdlib/Lean/Elab/PreDefinition/Main.c
generated
252
stage0/stdlib/Lean/Elab/PreDefinition/Main.c
generated
|
|
@ -16,11 +16,11 @@ extern "C" {
|
|||
lean_object* l_Lean_Elab_WF_TerminationBy_markAsUsed(lean_object*, lean_object*);
|
||||
lean_object* l_List_reverse___rarg(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_AssocList_contains___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__13___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_forallTelescope___at___private_Lean_Elab_Term_0__Lean_Elab_Term_tryPureCoe_x3f___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__26___closed__5;
|
||||
size_t lean_usize_add(size_t, size_t);
|
||||
lean_object* l_List_forM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_addPreDefinitions___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_addPreDefinitions___spec__7___closed__1;
|
||||
static lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_getMVarsAtPreDef___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_addPreDefinitions___spec__9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -32,6 +32,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_instInhabitedTerminationHints;
|
|||
lean_object* l_Lean_Meta_withLCtx___at___private_Lean_Elab_Binders_0__Lean_Elab_Term_FunBinders_elabFunBinderViews___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_stringToMessageData(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_addPreDefinitions___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___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_mk_empty_array_with_capacity(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_addPreDefinitions___spec__21___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_addPreDefinitions___spec__13___rarg(lean_object*);
|
||||
|
|
@ -47,9 +48,8 @@ uint8_t lean_usize_dec_eq(size_t, size_t);
|
|||
lean_object* lean_array_uget(lean_object*, size_t);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_addSCC___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__21___boxed(lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__1___closed__6;
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_addPreDefinitions___spec__23___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__6;
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__3___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__18(lean_object*, lean_object*, lean_object*, size_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_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Term_quoteAutoTactic___spec__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_getMVarsAtPreDef___closed__2;
|
||||
|
|
@ -64,7 +64,6 @@ static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___
|
|||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___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_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_addPreDefinitions___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__18___lambda__1___closed__4;
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__2;
|
||||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__18___lambda__4___closed__4;
|
||||
lean_object* lean_st_ref_get(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_isNonRecursive___lambda__1___boxed(lean_object*, lean_object*);
|
||||
|
|
@ -76,13 +75,17 @@ LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortCommand___at___private_Lean_Elab_
|
|||
static lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_resetOnStack___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__23___closed__1;
|
||||
lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___spec__16(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__18___lambda__4___closed__6;
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__1;
|
||||
static lean_object* l_Lean_Elab_addPreDefinitions___closed__11;
|
||||
lean_object* lean_array_push(lean_object*, lean_object*);
|
||||
lean_object* lean_array_get_size(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_addPreDefinitions___spec__15___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_MessageData_ofList(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_addPreDefinitions___spec__21(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___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*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__4;
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT uint8_t l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_isNonRecursive___lambda__1(lean_object*, lean_object*);
|
||||
lean_object* l_Std_mkHashSetImp___rarg(lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__18___lambda__4___closed__5;
|
||||
|
|
@ -90,6 +93,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_p
|
|||
LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_addPreDefinitions___spec__20___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_MessageData_joinSep(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_getMainModule___rarg(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t lean_usize_dec_lt(size_t, size_t);
|
||||
lean_object* l_Lean_Elab_WF_TerminationHint_markAsUsed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_ensureNoUnassignedMVarsAtPreDef(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -107,11 +111,13 @@ lean_object* l_Lean_Elab_addAndCompileUnsafe(lean_object*, uint8_t, lean_object*
|
|||
size_t lean_uint64_to_usize(uint64_t);
|
||||
lean_object* l_Lean_Expr_FindImpl_findUnsafe_x3f(lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_addPreDefinitions___closed__7;
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___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_Lean_throwError___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__1___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_PreDefinition_Main___hyg_1823_(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_addPreDefinitions___spec__17___boxed(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__6;
|
||||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__18___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Lean_throwErrorAt___at_Lean_Elab_addPreDefinitions___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_ResolveName_resolveNamespace_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -130,14 +136,15 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefi
|
|||
LEAN_EXPORT uint8_t l_Std_AssocList_contains___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__13(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_expandMacroImpl_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_st_ref_take(lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_addPreDefinitions___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*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__4;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_getDataOf___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__7(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_HashMap_insert___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__12(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_getMVarsAtPreDef___closed__3;
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__3___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_addPreDefinitions___spec__2(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_WF_expandTerminationBy(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_addPreDefinitions___closed__10;
|
||||
|
|
@ -149,7 +156,6 @@ static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___
|
|||
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_addPreDefinitions___spec__22(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_updateLowLinkOf___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__18___lambda__1(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___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* l_Std_mkHashMapImp___rarg(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__16___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__27___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -159,10 +165,12 @@ static lean_object* l_Lean_Elab_throwAbortCommand___at___private_Lean_Elab_PreDe
|
|||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__16___closed__1;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___lambda__2(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_panic___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__2(lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__5;
|
||||
uint64_t l_Lean_Name_hash(lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___lambda__2___boxed__const__1;
|
||||
lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_Term_synthesizeSyntheticMVars_loop___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_collectMVarsAtPreDef(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescope___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___rarg___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_st_mk_ref(lean_object*, lean_object*);
|
||||
lean_object* l_instMonadControlReaderT___lambda__3___boxed(lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_addPreDefinitions___spec__19(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -173,7 +181,6 @@ lean_object* l_Std_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_obje
|
|||
LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_addPreDefinitions___spec__13(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__16___closed__3;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_updateLowLinkOf___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__18(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__5;
|
||||
extern lean_object* l_Lean_Elab_instInhabitedPreDefinition;
|
||||
lean_object* l_Lean_Elab_WF_TerminationHint_find_x3f(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_addSCC_add___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__22(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -182,7 +189,6 @@ lean_object* l_Lean_Elab_Term_getCurrMacroScope(lean_object*, lean_object*, lean
|
|||
lean_object* lean_array_to_list(lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Environment_contains(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux(lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_ReaderT_pure___at_Lean_Elab_liftMacroM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_collectMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_addPreDefinitions___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -203,6 +209,7 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitio
|
|||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__18___lambda__4___closed__13;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs(lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__18___lambda__4___closed__9;
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__3;
|
||||
size_t lean_usize_of_nat(lean_object*);
|
||||
lean_object* l_Lean_Elab_addAndCompilePartialRec(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_setEnv___at_Lean_Meta_setInlineAttribute___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -222,11 +229,11 @@ lean_object* l_List_redLength___rarg(lean_object*);
|
|||
LEAN_EXPORT lean_object* l_Lean_throwErrorAt___at_Lean_Elab_addPreDefinitions___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__18___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescope___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_addPreDefinitions___spec__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__26(lean_object*, size_t, size_t, lean_object*);
|
||||
lean_object* lean_environment_main_module(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_addPreDefinitions___spec__4___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__3;
|
||||
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_addPreDefinitions___spec__23(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_instMonadControlT___rarg(lean_object*, lean_object*);
|
||||
|
|
@ -243,6 +250,7 @@ static lean_object* l_Lean_Elab_addPreDefinitions___closed__1;
|
|||
LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_addPreDefinitions___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Term_Quotation_getAntiquotationIds___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__3;
|
||||
lean_object* lean_nat_mul(lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__18___lambda__4___closed__1;
|
||||
lean_object* l_Lean_Elab_WF_TerminationHint_ensureAllUsed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -251,9 +259,8 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_c
|
|||
LEAN_EXPORT lean_object* l_Std_HashMapImp_expand___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__14(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_HashMapImp_moveEntries___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__15(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Std_AssocList_replace___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__17(lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__4;
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__2;
|
||||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__18___lambda__4___closed__3;
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__26___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*);
|
||||
|
|
@ -263,7 +270,6 @@ LEAN_EXPORT lean_object* l_Lean_SCC_scc___at___private_Lean_Elab_PreDefinition_M
|
|||
lean_object* lean_panic_fn(lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__18___lambda__4___closed__15;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_addPreDefinitions___spec__4___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___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_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_addPreDefinitions___spec__11___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_resetOnStack___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__23(lean_object*, lean_object*);
|
||||
lean_object* lean_mk_array(lean_object*, lean_object*);
|
||||
|
|
@ -284,15 +290,15 @@ static lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinitio
|
|||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__16___closed__4;
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_addPreDefinitions___lambda__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_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__18___lambda__5(lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___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_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__27(lean_object*, size_t, size_t, lean_object*);
|
||||
static lean_object* l_Lean_Elab_addPreDefinitions___closed__13;
|
||||
lean_object* l_Lean_Elab_WF_TerminationBy_find_x3f(lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__1___closed__2;
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_addPreDefinitions___spec__4___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_getMVarsAtPreDef(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_WF_expandTerminationHint___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescope___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__26___lambda__1___boxed(lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_isNonRecursive___boxed(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_addPreDefinitions___spec__3(size_t, size_t, size_t, lean_object*);
|
||||
|
|
@ -300,17 +306,15 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_addPreDefinitions___sp
|
|||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__16(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Std_mkHashMap___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__24(lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__4(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
|
||||
static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_addPreDefinitions___spec__8___rarg___closed__1;
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___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_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_addPreDefinitions___spec__13___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_setMCtx(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_indentExpr(lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__4;
|
||||
static lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__26___closed__3;
|
||||
static lean_object* l_Lean_Elab_addPreDefinitions___closed__2;
|
||||
LEAN_EXPORT lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_addSCC_add___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__22___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Lean_Elab_addPreDefinitions___closed__12;
|
||||
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
|
||||
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_WF_registerEqnsInfo___spec__1(size_t, size_t, lean_object*);
|
||||
|
|
@ -321,7 +325,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_TerminationHints_decreasingBy_x3f___default
|
|||
lean_object* l_instMonadControlT__1___rarg(lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__1___closed__1;
|
||||
LEAN_EXPORT lean_object* l_List_forM___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__20(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__1;
|
||||
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_Elab_addPreDefinitions___spec__17(lean_object*, size_t, size_t);
|
||||
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_addPreDefinitions___spec__4___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_getBetterRef(lean_object*, lean_object*);
|
||||
|
|
@ -363,7 +366,80 @@ x_1 = l_Lean_Elab_instInhabitedTerminationHints___closed__1;
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___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, lean_object* x_10, lean_object* x_11, lean_object* x_12) {
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescope___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___rarg___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_11;
|
||||
x_11 = lean_apply_9(x_1, x_4, x_5, x_2, x_3, x_6, x_7, x_8, x_9, x_10);
|
||||
return x_11;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescope___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___rarg(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; uint8_t x_12; lean_object* x_13;
|
||||
x_10 = lean_alloc_closure((void*)(l_Lean_Meta_forallTelescope___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___rarg___lambda__1), 10, 3);
|
||||
lean_closure_set(x_10, 0, x_2);
|
||||
lean_closure_set(x_10, 1, x_3);
|
||||
lean_closure_set(x_10, 2, x_4);
|
||||
x_11 = lean_box(0);
|
||||
x_12 = 0;
|
||||
x_13 = l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux___rarg(x_12, x_11, x_1, x_10, x_5, x_6, x_7, x_8, x_9);
|
||||
if (lean_obj_tag(x_13) == 0)
|
||||
{
|
||||
uint8_t x_14;
|
||||
x_14 = !lean_is_exclusive(x_13);
|
||||
if (x_14 == 0)
|
||||
{
|
||||
return x_13;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_15; lean_object* x_16; lean_object* x_17;
|
||||
x_15 = lean_ctor_get(x_13, 0);
|
||||
x_16 = lean_ctor_get(x_13, 1);
|
||||
lean_inc(x_16);
|
||||
lean_inc(x_15);
|
||||
lean_dec(x_13);
|
||||
x_17 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_17, 0, x_15);
|
||||
lean_ctor_set(x_17, 1, x_16);
|
||||
return x_17;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_18;
|
||||
x_18 = !lean_is_exclusive(x_13);
|
||||
if (x_18 == 0)
|
||||
{
|
||||
return x_13;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_19; lean_object* x_20; lean_object* x_21;
|
||||
x_19 = lean_ctor_get(x_13, 0);
|
||||
x_20 = lean_ctor_get(x_13, 1);
|
||||
lean_inc(x_20);
|
||||
lean_inc(x_19);
|
||||
lean_dec(x_13);
|
||||
x_21 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_21, 0, x_19);
|
||||
lean_ctor_set(x_21, 1, x_20);
|
||||
return x_21;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescope___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_Lean_Meta_forallTelescope___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___rarg), 9, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___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* x_12) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; uint8_t x_18; uint8_t x_19; lean_object* x_20;
|
||||
|
|
@ -388,7 +464,7 @@ x_20 = l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux(x_17,
|
|||
return x_20;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__1() {
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -396,16 +472,16 @@ x_1 = lean_mk_string("inhabitant for ");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__2() {
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__1;
|
||||
x_1 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__1;
|
||||
x_2 = l_Lean_stringToMessageData(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__3() {
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -413,16 +489,16 @@ x_1 = lean_mk_string("");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__4() {
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__3;
|
||||
x_1 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__3;
|
||||
x_2 = l_Lean_stringToMessageData(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___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, lean_object* x_11, lean_object* x_12) {
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___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, lean_object* x_11, lean_object* x_12) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_13; lean_object* x_14;
|
||||
|
|
@ -487,7 +563,7 @@ if (x_17 == 0)
|
|||
lean_object* x_19; lean_object* x_20;
|
||||
lean_dec(x_3);
|
||||
x_19 = lean_box(0);
|
||||
x_20 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__1(x_1, x_13, x_2, x_15, x_19, x_6, x_7, x_8, x_9, x_10, x_11, x_18);
|
||||
x_20 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__1(x_1, x_13, x_2, x_15, x_19, x_6, x_7, x_8, x_9, x_10, x_11, x_18);
|
||||
lean_dec(x_1);
|
||||
return x_20;
|
||||
}
|
||||
|
|
@ -497,11 +573,11 @@ lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean
|
|||
lean_inc(x_13);
|
||||
x_21 = lean_alloc_ctor(4, 1, 0);
|
||||
lean_ctor_set(x_21, 0, x_13);
|
||||
x_22 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__2;
|
||||
x_22 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__2;
|
||||
x_23 = lean_alloc_ctor(10, 2, 0);
|
||||
lean_ctor_set(x_23, 0, x_22);
|
||||
lean_ctor_set(x_23, 1, x_21);
|
||||
x_24 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__4;
|
||||
x_24 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__4;
|
||||
x_25 = lean_alloc_ctor(10, 2, 0);
|
||||
lean_ctor_set(x_25, 0, x_23);
|
||||
lean_ctor_set(x_25, 1, x_24);
|
||||
|
|
@ -511,7 +587,7 @@ lean_inc(x_27);
|
|||
x_28 = lean_ctor_get(x_26, 1);
|
||||
lean_inc(x_28);
|
||||
lean_dec(x_26);
|
||||
x_29 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__1(x_1, x_13, x_2, x_15, x_27, x_6, x_7, x_8, x_9, x_10, x_11, x_28);
|
||||
x_29 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__1(x_1, x_13, x_2, x_15, x_27, x_6, x_7, x_8, x_9, x_10, x_11, x_28);
|
||||
lean_dec(x_27);
|
||||
lean_dec(x_1);
|
||||
return x_29;
|
||||
|
|
@ -552,7 +628,7 @@ return x_45;
|
|||
}
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__3___closed__1() {
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__3___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
|
|
@ -562,18 +638,18 @@ lean_ctor_set(x_2, 0, x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__3(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_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__3(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_11; lean_object* x_12; lean_object* x_13;
|
||||
x_11 = lean_ctor_get(x_1, 4);
|
||||
lean_inc(x_11);
|
||||
lean_inc(x_11);
|
||||
x_12 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2), 12, 3);
|
||||
x_12 = lean_alloc_closure((void*)(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2), 12, 3);
|
||||
lean_closure_set(x_12, 0, x_1);
|
||||
lean_closure_set(x_12, 1, x_11);
|
||||
lean_closure_set(x_12, 2, x_2);
|
||||
x_13 = l_Lean_Meta_forallTelescope___at___private_Lean_Elab_Term_0__Lean_Elab_Term_tryPureCoe_x3f___spec__1___rarg(x_11, x_12, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
|
||||
x_13 = l_Lean_Meta_forallTelescope___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___rarg(x_11, x_12, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
|
||||
if (lean_obj_tag(x_13) == 0)
|
||||
{
|
||||
uint8_t x_14;
|
||||
|
|
@ -583,7 +659,7 @@ if (x_14 == 0)
|
|||
lean_object* x_15; lean_object* x_16;
|
||||
x_15 = lean_ctor_get(x_13, 0);
|
||||
lean_dec(x_15);
|
||||
x_16 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__3___closed__1;
|
||||
x_16 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__3___closed__1;
|
||||
lean_ctor_set(x_13, 0, x_16);
|
||||
return x_13;
|
||||
}
|
||||
|
|
@ -593,7 +669,7 @@ lean_object* x_17; lean_object* x_18; lean_object* x_19;
|
|||
x_17 = lean_ctor_get(x_13, 1);
|
||||
lean_inc(x_17);
|
||||
lean_dec(x_13);
|
||||
x_18 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__3___closed__1;
|
||||
x_18 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__3___closed__1;
|
||||
x_19 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_19, 0, x_18);
|
||||
lean_ctor_set(x_19, 1, x_17);
|
||||
|
|
@ -624,7 +700,7 @@ return x_23;
|
|||
}
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__1() {
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -632,17 +708,17 @@ x_1 = lean_mk_string("Elab");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__2() {
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__1;
|
||||
x_2 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__3() {
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -650,17 +726,17 @@ x_1 = lean_mk_string("definition");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__4() {
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__2;
|
||||
x_2 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__3;
|
||||
x_1 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__2;
|
||||
x_2 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__3;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__5() {
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -668,16 +744,16 @@ x_1 = lean_mk_string("processing ");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__6() {
|
||||
static lean_object* _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__6() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__5;
|
||||
x_1 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__5;
|
||||
x_2 = l_Lean_stringToMessageData(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1(lean_object* x_1, size_t x_2, size_t 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_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2(lean_object* x_1, size_t x_2, size_t 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) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_12;
|
||||
|
|
@ -701,7 +777,7 @@ else
|
|||
lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_63; lean_object* x_64; lean_object* x_65; uint8_t x_66;
|
||||
lean_dec(x_4);
|
||||
x_14 = lean_array_uget(x_1, x_3);
|
||||
x_15 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__4;
|
||||
x_15 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__4;
|
||||
x_63 = lean_st_ref_get(x_10, x_11);
|
||||
x_64 = lean_ctor_get(x_63, 0);
|
||||
lean_inc(x_64);
|
||||
|
|
@ -751,7 +827,7 @@ lean_inc(x_8);
|
|||
lean_inc(x_7);
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_5);
|
||||
x_19 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__3(x_14, x_15, x_18, x_5, x_6, x_7, x_8, x_9, x_10, x_17);
|
||||
x_19 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__3(x_14, x_15, x_18, x_5, x_6, x_7, x_8, x_9, x_10, x_17);
|
||||
if (lean_obj_tag(x_19) == 0)
|
||||
{
|
||||
lean_object* x_20;
|
||||
|
|
@ -846,11 +922,11 @@ x_36 = lean_ctor_get(x_14, 3);
|
|||
lean_inc(x_36);
|
||||
x_37 = lean_alloc_ctor(4, 1, 0);
|
||||
lean_ctor_set(x_37, 0, x_36);
|
||||
x_38 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__6;
|
||||
x_38 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__6;
|
||||
x_39 = lean_alloc_ctor(10, 2, 0);
|
||||
lean_ctor_set(x_39, 0, x_38);
|
||||
lean_ctor_set(x_39, 1, x_37);
|
||||
x_40 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__4;
|
||||
x_40 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__4;
|
||||
x_41 = lean_alloc_ctor(10, 2, 0);
|
||||
lean_ctor_set(x_41, 0, x_39);
|
||||
lean_ctor_set(x_41, 1, x_40);
|
||||
|
|
@ -866,7 +942,7 @@ lean_inc(x_8);
|
|||
lean_inc(x_7);
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_5);
|
||||
x_45 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__3(x_14, x_15, x_43, x_5, x_6, x_7, x_8, x_9, x_10, x_44);
|
||||
x_45 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__3(x_14, x_15, x_43, x_5, x_6, x_7, x_8, x_9, x_10, x_44);
|
||||
lean_dec(x_43);
|
||||
if (lean_obj_tag(x_45) == 0)
|
||||
{
|
||||
|
|
@ -974,7 +1050,7 @@ lean_inc(x_5);
|
|||
lean_inc(x_4);
|
||||
lean_inc(x_3);
|
||||
lean_inc(x_2);
|
||||
x_13 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1(x_1, x_10, x_11, x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
x_13 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2(x_1, x_10, x_11, x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
|
||||
if (lean_obj_tag(x_13) == 0)
|
||||
{
|
||||
lean_object* x_14; lean_object* x_15;
|
||||
|
|
@ -1015,26 +1091,26 @@ return x_19;
|
|||
}
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___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, lean_object* x_10, lean_object* x_11, lean_object* x_12) {
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___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* x_12) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_13;
|
||||
x_13 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
|
||||
x_13 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_1);
|
||||
return x_13;
|
||||
}
|
||||
}
|
||||
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__3___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_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__3___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_11;
|
||||
x_11 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__3(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
|
||||
x_11 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__3(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_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___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_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___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) {
|
||||
_start:
|
||||
{
|
||||
size_t x_12; size_t x_13; lean_object* x_14;
|
||||
|
|
@ -1042,7 +1118,7 @@ x_12 = lean_unbox_usize(x_2);
|
|||
lean_dec(x_2);
|
||||
x_13 = lean_unbox_usize(x_3);
|
||||
lean_dec(x_3);
|
||||
x_14 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1(x_1, x_12, x_13, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
|
||||
x_14 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2(x_1, x_12, x_13, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
|
||||
lean_dec(x_1);
|
||||
return x_14;
|
||||
}
|
||||
|
|
@ -3596,7 +3672,7 @@ static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefiniti
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__4;
|
||||
x_1 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__4;
|
||||
x_2 = l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__1___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
|
|
@ -3713,7 +3789,7 @@ x_22 = lean_ctor_get(x_14, 3);
|
|||
lean_inc(x_22);
|
||||
x_23 = lean_alloc_ctor(4, 1, 0);
|
||||
lean_ctor_set(x_23, 0, x_22);
|
||||
x_24 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__4;
|
||||
x_24 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__4;
|
||||
x_25 = lean_alloc_ctor(10, 2, 0);
|
||||
lean_ctor_set(x_25, 0, x_24);
|
||||
lean_ctor_set(x_25, 1, x_23);
|
||||
|
|
@ -5096,7 +5172,7 @@ x_33 = l_Lean_indentExpr(x_15);
|
|||
x_34 = lean_alloc_ctor(10, 2, 0);
|
||||
lean_ctor_set(x_34, 0, x_32);
|
||||
lean_ctor_set(x_34, 1, x_33);
|
||||
x_35 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__4;
|
||||
x_35 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__4;
|
||||
x_36 = lean_alloc_ctor(10, 2, 0);
|
||||
lean_ctor_set(x_36, 0, x_34);
|
||||
lean_ctor_set(x_36, 1, x_35);
|
||||
|
|
@ -5342,7 +5418,7 @@ lean_ctor_set(x_12, 1, x_11);
|
|||
x_13 = lean_alloc_ctor(10, 2, 0);
|
||||
lean_ctor_set(x_13, 0, x_12);
|
||||
lean_ctor_set(x_13, 1, x_2);
|
||||
x_14 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__4;
|
||||
x_14 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__4;
|
||||
x_15 = lean_alloc_ctor(10, 2, 0);
|
||||
lean_ctor_set(x_15, 0, x_13);
|
||||
lean_ctor_set(x_15, 1, x_14);
|
||||
|
|
@ -6837,7 +6913,7 @@ static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefiniti
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__4;
|
||||
x_1 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__4;
|
||||
x_2 = l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__18___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
|
|
@ -7022,7 +7098,7 @@ x_46 = lean_box(0);
|
|||
x_47 = l_List_mapTRAux___at_Lean_Meta_substCore___spec__6(x_45, x_46);
|
||||
x_48 = l_Lean_MessageData_ofList(x_47);
|
||||
lean_dec(x_47);
|
||||
x_49 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__4;
|
||||
x_49 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__4;
|
||||
x_50 = lean_alloc_ctor(10, 2, 0);
|
||||
lean_ctor_set(x_50, 0, x_49);
|
||||
lean_ctor_set(x_50, 1, x_48);
|
||||
|
|
@ -8494,28 +8570,28 @@ l_Lean_Elab_instInhabitedTerminationHints___closed__1 = _init_l_Lean_Elab_instIn
|
|||
lean_mark_persistent(l_Lean_Elab_instInhabitedTerminationHints___closed__1);
|
||||
l_Lean_Elab_instInhabitedTerminationHints = _init_l_Lean_Elab_instInhabitedTerminationHints();
|
||||
lean_mark_persistent(l_Lean_Elab_instInhabitedTerminationHints);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__1 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__1();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__1);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__2 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__2();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__2);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__3 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__3();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__3);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__4 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__4();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__2___closed__4);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__3___closed__1 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__3___closed__1();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___lambda__3___closed__1);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__1 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__1();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__1);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__2 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__2();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__2);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__3 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__3();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__3);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__4 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__4();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__4);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__5 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__5();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__5);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__6 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__6();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__1___closed__6);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__1 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__1();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__1);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__2 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__2();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__2);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__3 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__3();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__3);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__4 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__4();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__4);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__3___closed__1 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__3___closed__1();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__3___closed__1);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__1 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__1();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__1);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__2 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__2();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__2);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__3 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__3();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__3);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__4 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__4();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__4);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__5 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__5();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__5);
|
||||
l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__6 = _init_l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__6();
|
||||
lean_mark_persistent(l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___closed__6);
|
||||
l___private_Lean_Util_SCC_0__Lean_SCC_getDataOf___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__7___closed__1 = _init_l___private_Lean_Util_SCC_0__Lean_SCC_getDataOf___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__7___closed__1();
|
||||
lean_mark_persistent(l___private_Lean_Util_SCC_0__Lean_SCC_getDataOf___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__7___closed__1);
|
||||
l___private_Lean_Util_SCC_0__Lean_SCC_resetOnStack___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__23___closed__1 = _init_l___private_Lean_Util_SCC_0__Lean_SCC_resetOnStack___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__23___closed__1();
|
||||
|
|
|
|||
6743
stage0/stdlib/Lean/Elab/Term.c
generated
6743
stage0/stdlib/Lean/Elab/Term.c
generated
File diff suppressed because it is too large
Load diff
Loading…
Add table
Reference in a new issue