chore: update stage0
This commit is contained in:
parent
110b014752
commit
fdf5c3280e
30 changed files with 7459 additions and 10379 deletions
3
stage0/src/Init/Data/Array/Basic.lean
generated
3
stage0/src/Init/Data/Array/Basic.lean
generated
|
|
@ -45,6 +45,9 @@ def back [Inhabited α] (a : Array α) : α :=
|
|||
def get? (a : Array α) (i : Nat) : Option α :=
|
||||
if h : i < a.size then some (a.get ⟨i, h⟩) else none
|
||||
|
||||
def back? (a : Array α) : Option α :=
|
||||
a.get? (a.size - 1)
|
||||
|
||||
-- auxiliary declaration used in the equation compiler when pattern matching array literals.
|
||||
abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
|
||||
a.get ⟨i, h₁.symm ▸ h₂⟩
|
||||
|
|
|
|||
16
stage0/src/Lean/ParserCompiler.lean
generated
16
stage0/src/Lean/ParserCompiler.lean
generated
|
|
@ -24,9 +24,12 @@ structure Context (α : Type) where
|
|||
|
||||
def Context.tyName {α} (ctx : Context α) : Name := ctx.categoryAttr.defn.valueTypeName
|
||||
|
||||
-- replace all references of `Parser` with `tyName` as a first approximation
|
||||
def preprocessParserBody {α} (ctx : Context α) (e : Expr) : Expr :=
|
||||
e.replace fun e => if e.isConstOf `Lean.Parser.Parser then mkConst ctx.tyName else none
|
||||
-- replace all references of `Parser` with `tyName`
|
||||
def replaceParserTy {α} (ctx : Context α) (e : Expr) : Expr :=
|
||||
e.replace fun e =>
|
||||
-- strip `optParam`
|
||||
let e := if e.isOptParam then e.appFn!.appArg! else e
|
||||
if e.isConstOf `Lean.Parser.Parser then mkConst ctx.tyName else none
|
||||
|
||||
section
|
||||
open Meta
|
||||
|
|
@ -73,13 +76,10 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
|
|||
| throwError! "don't know how to generate {ctx.varName} for non-definition '{e}'"
|
||||
unless (env.getModuleIdxFor? c).isNone || force do
|
||||
throwError! "refusing to generate code for imported parser declaration '{c}'; use `@[runParserAttributeHooks]` on its definition instead."
|
||||
let value ← compileParserExpr $ preprocessParserBody ctx value
|
||||
let value ← compileParserExpr $ replaceParserTy ctx value
|
||||
let ty ← forallTelescope cinfo.type fun params _ =>
|
||||
params.foldrM (init := mkConst ctx.tyName) fun param ty => do
|
||||
let paramTy ← inferType param;
|
||||
let paramTy ← forallTelescope paramTy fun _ b => pure $
|
||||
if b.isConstOf `Lean.Parser.Parser then mkConst ctx.tyName
|
||||
else b
|
||||
let paramTy ← replaceParserTy ctx <$> inferType param
|
||||
pure $ mkForall `_ BinderInfo.default paramTy ty
|
||||
let decl := Declaration.defnDecl {
|
||||
name := c', lparams := [],
|
||||
|
|
|
|||
12
stage0/src/Lean/Syntax.lean
generated
12
stage0/src/Lean/Syntax.lean
generated
|
|
@ -257,10 +257,6 @@ structure Traverser where
|
|||
|
||||
namespace Traverser
|
||||
|
||||
-- TODO(Kha): check this
|
||||
def idxsBack (t : Traverser) : Nat :=
|
||||
if t.idxs.isEmpty then 0 else t.idxs.back
|
||||
|
||||
def fromSyntax (stx : Syntax) : Traverser :=
|
||||
⟨stx, #[], #[]⟩
|
||||
|
||||
|
|
@ -277,7 +273,7 @@ def down (t : Traverser) (idx : Nat) : Traverser :=
|
|||
/-- Advance to the parent of the current node, if any. -/
|
||||
def up (t : Traverser) : Traverser :=
|
||||
if t.parents.size > 0 then
|
||||
let cur := if t.idxsBack < t.parents.back.getNumArgs then t.parents.back.setArg t.idxsBack t.cur else t.parents.back
|
||||
let cur := if t.idxs.back < t.parents.back.getNumArgs then t.parents.back.setArg t.idxs.back t.cur else t.parents.back
|
||||
{ cur := cur, parents := t.parents.pop, idxs := t.idxs.pop }
|
||||
else
|
||||
t
|
||||
|
|
@ -285,14 +281,14 @@ def up (t : Traverser) : Traverser :=
|
|||
/-- Advance to the left sibling of the current node, if any. -/
|
||||
def left (t : Traverser) : Traverser :=
|
||||
if t.parents.size > 0 then
|
||||
t.up.down (t.idxsBack - 1)
|
||||
t.up.down (t.idxs.back - 1)
|
||||
else
|
||||
t
|
||||
|
||||
/-- Advance to the right sibling of the current node, if any. -/
|
||||
def right (t : Traverser) : Traverser :=
|
||||
if t.parents.size > 0 then
|
||||
t.up.down (t.idxsBack + 1)
|
||||
t.up.down (t.idxs.back + 1)
|
||||
else
|
||||
t
|
||||
|
||||
|
|
@ -315,7 +311,7 @@ def goRight : m Unit := @modify _ _ t.st (fun t => t.right)
|
|||
|
||||
def getIdx : m Nat := do
|
||||
let st ← t.st.get
|
||||
pure st.idxsBack
|
||||
st.idxs.back?.getD 0
|
||||
|
||||
end MonadTraverser
|
||||
end Syntax
|
||||
|
|
|
|||
2
stage0/stdlib/CMakeLists.txt
generated
2
stage0/stdlib/CMakeLists.txt
generated
File diff suppressed because one or more lines are too long
147
stage0/stdlib/Init/Data/Array/Basic.c
generated
147
stage0/stdlib/Init/Data/Array/Basic.c
generated
|
|
@ -34,6 +34,7 @@ lean_object* l_Array_indexOfAux___rarg(lean_object*, lean_object*, lean_object*,
|
|||
lean_object* l_term_x23_x5b___x2c_x5d___closed__3;
|
||||
lean_object* l_Array_filterMapM___at_Array_filterMap___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_filterMapM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_back_x3f(lean_object*);
|
||||
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
|
||||
lean_object* l_Array_forM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_nat_div(lean_object*, lean_object*);
|
||||
|
|
@ -152,6 +153,7 @@ lean_object* l_Array_forM___rarg___boxed(lean_object*, lean_object*, lean_object
|
|||
lean_object* l_Array_mapM(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_mapIdxM_map_match__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_term_x23_x5b___x2c_x5d___closed__2;
|
||||
lean_object* l_Array_back_x3f___rarg(lean_object*);
|
||||
lean_object* l_Array_getIdx_x3f(lean_object*);
|
||||
extern lean_object* l_term_x5b___x2c_x5d___closed__2;
|
||||
lean_object* l_Array_foldrMUnsafe___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -163,7 +165,6 @@ lean_object* l_Array_allM(lean_object*, lean_object*);
|
|||
lean_object* l_Array_mapMUnsafe_map___at_Array_map___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_allM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyMUnsafe_any___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
lean_object* l_Array_isEqvAux(lean_object*);
|
||||
lean_object* l_Array_forIn(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyM_loop___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
|
||||
|
|
@ -175,6 +176,7 @@ lean_object* l_Array_mapIdx___rarg(lean_object*, lean_object*);
|
|||
lean_object* l_Array_getMax_x3f___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_redLength_match__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_swap___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
lean_object* l_Array_foldrMUnsafe_fold___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_mapIdxM_map___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Data_Array_Basic_0__Array_allDiffAuxAux___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -196,6 +198,7 @@ lean_object* l_Array_foldrM___rarg___boxed(lean_object*, lean_object*, lean_obje
|
|||
lean_object* l_Array_getLit(lean_object*, lean_object*);
|
||||
uint8_t l_Array_isPrefixOf___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_insertAtAux_match__1(lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__1;
|
||||
lean_object* l_Array_forIn_loop_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_foldrMUnsafe_fold___at_Array_foldr___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Array_forInUnsafe_loop___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
|
||||
|
|
@ -212,7 +215,6 @@ lean_object* l_Array_mapMUnsafe_map___rarg___lambda__1___boxed(lean_object*, lea
|
|||
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findIdx_x3f_loop_match__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_forIn___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__1;
|
||||
lean_object* l___private_Init_Data_Array_Basic_0__Array_allDiffAuxAux(lean_object*);
|
||||
lean_object* l_Array_eraseIdxAux_match__1(lean_object*, lean_object*);
|
||||
lean_object* l_Array_forInUnsafe(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -228,13 +230,13 @@ lean_object* l_Array_forInUnsafe_loop_match__1(lean_object*, lean_object*);
|
|||
lean_object* l_Array_filter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_eraseIdx_x27___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__4;
|
||||
lean_object* l_Array_getIdx_x3f___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_anyMUnsafe_any___at_Array_all___spec__1(lean_object*);
|
||||
lean_object* l_Array_get_x3f___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findIdx_x3f___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_mapM___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_insertAtAux_match__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__2;
|
||||
lean_object* l_Array_findRev_x3f(lean_object*);
|
||||
lean_object* l_Array_mapMUnsafe_map(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_foldlMUnsafe_fold___at_Array_filter___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -256,11 +258,10 @@ lean_object* l_Array_forInUnsafe_loop___at_Array_findM_x3f___spec__1___rarg___la
|
|||
lean_object* l_Array_forInUnsafe_loop___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_instReprArray___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Array_append___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__8;
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__8;
|
||||
lean_object* l_Array_feraseIdx(lean_object*);
|
||||
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_foldlMUnsafe_fold___at_Array_filterM___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__2;
|
||||
lean_object* l_Array_forIn_loop_match__2(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_forIn_loop_match__2___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_foldlMUnsafe_fold___at_Array_filter___spec__1___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*);
|
||||
|
|
@ -305,9 +306,11 @@ lean_object* l_Array_back___rarg(lean_object*, lean_object*);
|
|||
lean_object* l_Array_anyMUnsafe_any___at_Array_allM___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevM_x3f_find___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_filterMap(lean_object*, lean_object*);
|
||||
lean_object* l_Array_back_x3f___rarg___boxed(lean_object*);
|
||||
lean_object* l_Array_anyMUnsafe_any___at_Array_allM___spec__1___rarg___lambda__1(lean_object*, uint8_t);
|
||||
lean_object* l_Array_findSomeM_x3f___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_array_to_list(lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__4;
|
||||
lean_object* l_Array_eraseIdxSzAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_eraseIdxSzAux(lean_object*);
|
||||
lean_object* l_Array_modify___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -326,7 +329,6 @@ uint8_t l_Array_anyMUnsafe_any___at_Array_any___spec__1___rarg(lean_object*, lea
|
|||
extern lean_object* l_myMacro____x40_Init_Notation___hyg_38____closed__8;
|
||||
lean_object* l_Array_findRevM_x3f(lean_object*, lean_object*);
|
||||
lean_object* l_Array_forInUnsafe_loop_match__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__6;
|
||||
lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Data_Array_Basic_0__Array_allDiffAuxAux_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_reverse___rarg(lean_object*);
|
||||
|
|
@ -363,6 +365,7 @@ lean_object* l_Array_mapMUnsafe_map___at_Array_map___spec__1(lean_object*, lean_
|
|||
lean_object* l_Array_findSome_x21___rarg___closed__1;
|
||||
lean_object* l_Array_insertAt___rarg___closed__2;
|
||||
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__6;
|
||||
lean_object* l_Array_anyMUnsafe___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_term_x5b___x2c_x5d___closed__3;
|
||||
lean_object* l_Array_foldlMUnsafe_fold___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, size_t, lean_object*);
|
||||
|
|
@ -407,7 +410,6 @@ lean_object* l_Array_zip(lean_object*, lean_object*);
|
|||
lean_object* l_ReaderT_instMonadReaderT___rarg___lambda__4___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_foldlM_loop(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_forIn_loop___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
lean_object* l_Array_shrink_loop___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Array_mapIdxM_map___at_Array_mapIdx___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevM_x3f_find_match__1(lean_object*, lean_object*);
|
||||
|
|
@ -427,6 +429,7 @@ lean_object* l_Array_partition___rarg___closed__1;
|
|||
lean_object* l_Array_getLit___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_foldlMUnsafe_fold___at_Array_filterM___spec__1___rarg___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t);
|
||||
lean_object* l_Array_modify(lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
lean_object* lean_list_to_array(lean_object*, lean_object*);
|
||||
extern lean_object* l_Id_instMonadId;
|
||||
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
|
||||
|
|
@ -439,6 +442,7 @@ lean_object* l_Array_shrink(lean_object*);
|
|||
lean_object* l_Array_isEmpty(lean_object*);
|
||||
uint8_t l_Array_any___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_foldr___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__3;
|
||||
lean_object* lean_panic_fn(lean_object*, lean_object*);
|
||||
lean_object* l_Array_forInUnsafe_loop(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_redLength(lean_object*);
|
||||
|
|
@ -461,7 +465,6 @@ lean_object* l_Array_findSomeRevM_x3f_find_match__2___rarg(lean_object*, lean_ob
|
|||
lean_object* l_Array_isPrefixOf___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_foldlMUnsafe(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_reverse_rev___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__3;
|
||||
lean_object* l_Array_zipWithAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_foldlMUnsafe_fold___at_Array_filter___spec__1(lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Notation___hyg_7116____closed__5;
|
||||
|
|
@ -485,7 +488,6 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Array_append___spec__1___rarg___boxe
|
|||
lean_object* l_Array_mapIdx___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRev_x3f___rarg___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSomeRevM_x3f_find___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__7;
|
||||
lean_object* l_Array_forRevM(lean_object*, lean_object*);
|
||||
lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*);
|
||||
lean_object* l___private_Init_Data_Array_Basic_0__Array_allDiffAuxAux_match__1(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -520,6 +522,7 @@ lean_object* l_Array_anyM_loop_match__1(lean_object*);
|
|||
lean_object* l_Array_forInUnsafe_loop___at_Array_findIdxM_x3f___spec__1___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_filterMapM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_eraseIdxSzAuxInstance(lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__7;
|
||||
lean_object* l_Array_instReprArray___rarg___closed__1;
|
||||
lean_object* l_Array_foldlM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_erase_match__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -550,6 +553,7 @@ lean_object* l_Array_isEqvAux_match__1___rarg___boxed(lean_object*, lean_object*
|
|||
lean_object* l_Array_contains(lean_object*);
|
||||
lean_object* l_Array_insertAtAux___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
lean_object* l_Array_forInUnsafe_loop___at_Array_find_x3f___spec__1___rarg(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*);
|
||||
lean_object* l_Array_foldlMUnsafe_fold___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_redLength_match__1(lean_object*, lean_object*);
|
||||
|
|
@ -575,7 +579,6 @@ lean_object* l_ReaderT_instMonadExceptOfReaderT___rarg___lambda__2(lean_object*,
|
|||
lean_object* l_Array_forInUnsafe_loop___at_Array_findIdxM_x3f___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_insertAt(lean_object*);
|
||||
lean_object* l_Array_elem(lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
lean_object* l_Array_zipWithAux___at_Array_zip___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_filter___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findSome_x21_match__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -585,7 +588,7 @@ lean_object* l_Array_foldrM_fold(lean_object*, lean_object*, lean_object*);
|
|||
lean_object* l_Array_insertAt___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_findIdxM_x3f_match__2(lean_object*);
|
||||
lean_object* l_Array_mapMUnsafe_map___at_Array_map___spec__1___rarg(lean_object*, size_t, size_t, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393_(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405_(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_contains___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_eraseIdxSzAux_match__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_foldrMUnsafe_fold___at_Array_toList___spec__1___rarg(lean_object*, size_t, size_t, lean_object*);
|
||||
|
|
@ -768,6 +771,36 @@ lean_dec(x_1);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_back_x3f___rarg(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_2 = lean_array_get_size(x_1);
|
||||
x_3 = lean_unsigned_to_nat(1u);
|
||||
x_4 = lean_nat_sub(x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
x_5 = l_Array_get_x3f___rarg(x_1, x_4);
|
||||
lean_dec(x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_back_x3f(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_Array_back_x3f___rarg___boxed), 1, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_back_x3f___rarg___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_Array_back_x3f___rarg(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_getLit___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -917,7 +950,7 @@ x_11 = l_Array_swapAt_x21___rarg___closed__2;
|
|||
x_12 = lean_string_append(x_10, x_11);
|
||||
x_13 = l_Array_swapAt_x21___rarg___closed__3;
|
||||
x_14 = l_Array_swapAt_x21___rarg___closed__4;
|
||||
x_15 = lean_unsigned_to_nat(90u);
|
||||
x_15 = lean_unsigned_to_nat(93u);
|
||||
x_16 = lean_unsigned_to_nat(4u);
|
||||
x_17 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_13, x_14, x_15, x_16, x_12);
|
||||
lean_dec(x_12);
|
||||
|
|
@ -5935,7 +5968,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_Array_swapAt_x21___rarg___closed__3;
|
||||
x_2 = l_Array_findSome_x21___rarg___closed__1;
|
||||
x_3 = lean_unsigned_to_nat(384u);
|
||||
x_3 = lean_unsigned_to_nat(387u);
|
||||
x_4 = lean_unsigned_to_nat(14u);
|
||||
x_5 = l_Array_findSome_x21___rarg___closed__2;
|
||||
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
|
||||
|
|
@ -7533,7 +7566,7 @@ x_1 = l_term_x23_x5b___x2c_x5d___closed__6;
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__1() {
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -7541,22 +7574,22 @@ x_1 = lean_mk_string("List.toArray");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__2() {
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__1;
|
||||
x_1 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__1;
|
||||
x_2 = lean_string_utf8_byte_size(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__3() {
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
|
||||
x_1 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__1;
|
||||
x_1 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__1;
|
||||
x_2 = lean_unsigned_to_nat(0u);
|
||||
x_3 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__2;
|
||||
x_3 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__2;
|
||||
x_4 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_4, 0, x_1);
|
||||
lean_ctor_set(x_4, 1, x_2);
|
||||
|
|
@ -7564,7 +7597,7 @@ lean_ctor_set(x_4, 2, x_3);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__4() {
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
|
|
@ -7572,41 +7605,41 @@ x_1 = lean_mk_string("toArray");
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5() {
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_myMacro____x40_Init_Notation___hyg_7116____closed__5;
|
||||
x_2 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__4;
|
||||
x_2 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__4;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__6() {
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__6() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
x_2 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_2);
|
||||
lean_ctor_set(x_3, 1, x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__7() {
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__7() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__6;
|
||||
x_2 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__6;
|
||||
x_3 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_2);
|
||||
lean_ctor_set(x_3, 1, x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__8() {
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__8() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
|
|
@ -7618,17 +7651,17 @@ lean_ctor_set(x_3, 1, x_2);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9() {
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Array_empty___closed__1;
|
||||
x_2 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__8;
|
||||
x_2 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__8;
|
||||
x_3 = lean_array_push(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10() {
|
||||
static lean_object* _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
|
|
@ -7640,7 +7673,7 @@ lean_ctor_set(x_3, 1, x_2);
|
|||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405_(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4; uint8_t x_5;
|
||||
|
|
@ -7671,11 +7704,11 @@ lean_inc(x_11);
|
|||
x_12 = lean_ctor_get(x_2, 1);
|
||||
lean_inc(x_12);
|
||||
lean_dec(x_2);
|
||||
x_13 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
x_13 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
x_14 = l_Lean_addMacroScope(x_12, x_13, x_11);
|
||||
x_15 = l_Lean_instInhabitedSourceInfo___closed__1;
|
||||
x_16 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__3;
|
||||
x_17 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__7;
|
||||
x_16 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__3;
|
||||
x_17 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__7;
|
||||
x_18 = lean_alloc_ctor(3, 4, 0);
|
||||
lean_ctor_set(x_18, 0, x_15);
|
||||
lean_ctor_set(x_18, 1, x_16);
|
||||
|
|
@ -7689,9 +7722,9 @@ x_22 = l_Lean_nullKind___closed__2;
|
|||
x_23 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_23, 0, x_22);
|
||||
lean_ctor_set(x_23, 1, x_21);
|
||||
x_24 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_24 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_25 = lean_array_push(x_24, x_23);
|
||||
x_26 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_26 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_27 = lean_array_push(x_25, x_26);
|
||||
x_28 = l_term_x5b___x2c_x5d___closed__2;
|
||||
x_29 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -9281,7 +9314,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_Array_swapAt_x21___rarg___closed__3;
|
||||
x_2 = l_Array_insertAt___rarg___closed__1;
|
||||
x_3 = lean_unsigned_to_nat(666u);
|
||||
x_3 = lean_unsigned_to_nat(669u);
|
||||
x_4 = lean_unsigned_to_nat(22u);
|
||||
x_5 = l_Array_insertAt___rarg___closed__2;
|
||||
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
|
||||
|
|
@ -10031,26 +10064,26 @@ l_term_x23_x5b___x2c_x5d___closed__6 = _init_l_term_x23_x5b___x2c_x5d___closed__
|
|||
lean_mark_persistent(l_term_x23_x5b___x2c_x5d___closed__6);
|
||||
l_term_x23_x5b___x2c_x5d = _init_l_term_x23_x5b___x2c_x5d();
|
||||
lean_mark_persistent(l_term_x23_x5b___x2c_x5d);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__1 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__1();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__1);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__2 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__2();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__2);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__3 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__3();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__3);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__4 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__4();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__4);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__6 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__6();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__6);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__7 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__7();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__7);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__8 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__8();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__8);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__1 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__1();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__1);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__2 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__2();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__2);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__3 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__3();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__3);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__4 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__4();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__4);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__6 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__6();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__6);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__7 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__7();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__7);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__8 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__8();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__8);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9);
|
||||
l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10 = _init_l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10();
|
||||
lean_mark_persistent(l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10);
|
||||
l_Array_partition___rarg___closed__1 = _init_l_Array_partition___rarg___closed__1();
|
||||
lean_mark_persistent(l_Array_partition___rarg___closed__1);
|
||||
l_Array_insertAt___rarg___closed__1 = _init_l_Array_insertAt___rarg___closed__1();
|
||||
|
|
|
|||
4
stage0/stdlib/Init/Meta.c
generated
4
stage0/stdlib/Init/Meta.c
generated
|
|
@ -356,7 +356,6 @@ lean_object* l_ReaderT_instMonadReaderT___rarg___lambda__4___boxed(lean_object*,
|
|||
lean_object* l_Lean_Syntax_mkApp___closed__1;
|
||||
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
|
||||
lean_object* l_Lean_Syntax_decodeQuotedChar_match__6(lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
lean_object* l___private_Init_Meta_0__Lean_quoteName_match__1(lean_object*);
|
||||
lean_object* l_Lean_Name_appendAfter(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_getSepArgs(lean_object*);
|
||||
|
|
@ -369,6 +368,7 @@ lean_object* l_Lean_instQuoteString___boxed(lean_object*);
|
|||
lean_object* l_Lean_Syntax_expandInterpolatedStrChunks___closed__1;
|
||||
lean_object* l_Lean_instQuoteBool___closed__2;
|
||||
lean_object* l_Lean_Syntax_expandInterpolatedStrChunks_match__3___rarg(lean_object*, lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
lean_object* l_Lean_Syntax_expandInterpolatedStrChunks___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Syntax_hasArgs(lean_object*);
|
||||
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Syntax_getSepArgs___spec__1(lean_object*, size_t, size_t, lean_object*);
|
||||
|
|
@ -9292,7 +9292,7 @@ x_3 = lean_array_to_list(lean_box(0), x_2);
|
|||
x_4 = l___private_Init_Meta_0__Lean_quoteList___rarg(x_1, x_3);
|
||||
x_5 = l_Lean_mkOptionalNode___closed__2;
|
||||
x_6 = lean_array_push(x_5, x_4);
|
||||
x_7 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
x_7 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
x_8 = l_Lean_Syntax_mkCApp(x_7, x_6);
|
||||
return x_8;
|
||||
}
|
||||
|
|
|
|||
10
stage0/stdlib/Init/NotationExtra.c
generated
10
stage0/stdlib/Init/NotationExtra.c
generated
|
|
@ -307,6 +307,7 @@ lean_object* l_Lean_expandExplicitBindersAux_loop___closed__4;
|
|||
lean_object* l_Lean_command__Unif__hint______Where___x7c_x2d_u22a2_____closed__9;
|
||||
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2140____closed__2;
|
||||
extern lean_object* l_Lean_Parser_Tactic_intro___closed__3;
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
lean_object* l_Lean_unbracktedExplicitBinders___closed__3;
|
||||
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2656____closed__1;
|
||||
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2492____boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -318,7 +319,6 @@ lean_object* l_Lean_command__Unif__hint______Where___x7c_x2d_u22a2_____closed__8
|
|||
lean_object* l_Lean_command__Unif__hint______Where___x7c_x2d_u22a2_____closed__17;
|
||||
lean_object* l_myMacro____x40_Init_NotationExtra___hyg_2656____closed__8;
|
||||
extern lean_object* l_Lean_Parser_Tactic_intro___closed__15;
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
lean_object* l_Lean_command__Unif__hint______Where___x7c_x2d_u22a2_____closed__1;
|
||||
lean_object* l_term_u2203___x2c_____closed__6;
|
||||
lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__39;
|
||||
|
|
@ -2693,7 +2693,7 @@ lean_ctor_set(x_199, 0, x_165);
|
|||
lean_ctor_set(x_199, 1, x_198);
|
||||
x_200 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_201 = lean_array_push(x_200, x_199);
|
||||
x_202 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_202 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_203 = lean_array_push(x_201, x_202);
|
||||
x_204 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_205 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -2803,7 +2803,7 @@ lean_ctor_set(x_264, 0, x_165);
|
|||
lean_ctor_set(x_264, 1, x_263);
|
||||
x_265 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_266 = lean_array_push(x_265, x_264);
|
||||
x_267 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_267 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_268 = lean_array_push(x_266, x_267);
|
||||
x_269 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_270 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -2991,7 +2991,7 @@ lean_ctor_set(x_59, 0, x_17);
|
|||
lean_ctor_set(x_59, 1, x_58);
|
||||
x_60 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_61 = lean_array_push(x_60, x_59);
|
||||
x_62 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_62 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_63 = lean_array_push(x_61, x_62);
|
||||
x_64 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_65 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -3091,7 +3091,7 @@ lean_ctor_set(x_120, 0, x_17);
|
|||
lean_ctor_set(x_120, 1, x_119);
|
||||
x_121 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_122 = lean_array_push(x_121, x_120);
|
||||
x_123 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_123 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_124 = lean_array_push(x_122, x_123);
|
||||
x_125 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_126 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
|
|||
2
stage0/stdlib/Lean/Compiler/IR/Basic.c
generated
2
stage0/stdlib/Lean/Compiler/IR/Basic.c
generated
|
|
@ -4076,7 +4076,7 @@ x_13 = l_Array_swapAt_x21___rarg___closed__2;
|
|||
x_14 = lean_string_append(x_12, x_13);
|
||||
x_15 = l_Array_swapAt_x21___rarg___closed__3;
|
||||
x_16 = l_Array_swapAt_x21___rarg___closed__4;
|
||||
x_17 = lean_unsigned_to_nat(90u);
|
||||
x_17 = lean_unsigned_to_nat(93u);
|
||||
x_18 = lean_unsigned_to_nat(4u);
|
||||
x_19 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_15, x_16, x_17, x_18, x_14);
|
||||
lean_dec(x_14);
|
||||
|
|
|
|||
4
stage0/stdlib/Lean/Elab/App.c
generated
4
stage0/stdlib/Lean/Elab/App.c
generated
|
|
@ -627,7 +627,6 @@ lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_mergeFailures_match__1_
|
|||
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppLValsAux_loop_match__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_whnf___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValAux___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*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(lean_object*);
|
||||
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_consumeImplicits___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_propagateExpectedType___closed__1;
|
||||
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_resolveLValAux_match__3(lean_object*);
|
||||
|
|
@ -698,6 +697,7 @@ uint8_t l_Lean_isStructureLike(lean_object*, lean_object*);
|
|||
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___closed__4;
|
||||
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_processExplictArg_match__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_mkBaseProjections___closed__2;
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
|
||||
lean_object* l_Lean_indentExpr(lean_object*);
|
||||
lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_propagateExpectedType___closed__6;
|
||||
lean_object* l_Lean_Elab_Term_expandPipeProj(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -33436,7 +33436,7 @@ x_90 = l_Array_isEmpty___rarg(x_89);
|
|||
if (x_90 == 0)
|
||||
{
|
||||
lean_object* x_91; lean_object* x_92; uint8_t x_93;
|
||||
x_91 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_89);
|
||||
x_91 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_89);
|
||||
x_92 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_expandApp___spec__1___closed__4;
|
||||
x_93 = l_Lean_Syntax_isOfKind(x_91, x_92);
|
||||
if (x_93 == 0)
|
||||
|
|
|
|||
4
stage0/stdlib/Lean/Elab/BuiltinNotation.c
generated
4
stage0/stdlib/Lean/Elab/BuiltinNotation.c
generated
|
|
@ -509,7 +509,6 @@ lean_object* lean_expr_abstract(lean_object*, lean_object*);
|
|||
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_getPropToDecide_match__1(lean_object*);
|
||||
extern lean_object* l_Lean_Syntax_expandInterpolatedStr___lambda__1___closed__2;
|
||||
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__2;
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabBorrowed___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_mkPairs___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabNativeRefl___lambda__1___closed__7;
|
||||
|
|
@ -580,6 +579,7 @@ lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParser
|
|||
lean_object* l_Lean_Elab_Term_elabSubst___lambda__1(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_expandAssert(lean_object*);
|
||||
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabCDot_match__1(lean_object*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandSorry(lean_object*);
|
||||
lean_object* l_Lean_indentExpr(lean_object*);
|
||||
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux___closed__2;
|
||||
|
|
@ -8575,7 +8575,7 @@ x_4 = lean_array_get_size(x_1);
|
|||
x_5 = lean_unsigned_to_nat(1u);
|
||||
x_6 = lean_nat_sub(x_4, x_5);
|
||||
lean_dec(x_4);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_1);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_1);
|
||||
x_8 = l_Lean_Elab_Term_mkPairs_loop(x_1, x_6, x_7, x_2, x_3);
|
||||
return x_8;
|
||||
}
|
||||
|
|
|
|||
6
stage0/stdlib/Lean/Elab/Declaration.c
generated
6
stage0/stdlib/Lean/Elab/Declaration.c
generated
|
|
@ -349,6 +349,7 @@ lean_object* l_Lean_Elab_Command_checkValidCtorModifier___at___private_Lean_Elab
|
|||
lean_object* l_Lean_Elab_Command_expandInitCmd___closed__25;
|
||||
lean_object* l_Lean_Meta_mkForallUsedOnlyImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
lean_object* l_Lean_Elab_Command_elabDeclaration___closed__5;
|
||||
lean_object* l_Lean_Elab_Command_elabInductive(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_List_isEmpty___rarg(lean_object*);
|
||||
|
|
@ -367,7 +368,6 @@ lean_object* l_Lean_Meta_mkForallUsedOnly___at_Lean_Elab_Command_elabAxiom___spe
|
|||
lean_object* l_Lean_Elab_Command_expandMutualElement_match__2___rarg(lean_object*, lean_object*);
|
||||
uint8_t l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_isMutualInductive(lean_object*);
|
||||
lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
lean_object* l_Lean_Elab_Command_expandMutualNamespace_match__3___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Elab_Command_expandInCmd___closed__2;
|
||||
|
|
@ -7654,7 +7654,7 @@ lean_ctor_set(x_79, 0, x_39);
|
|||
lean_ctor_set(x_79, 1, x_78);
|
||||
x_80 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_81 = lean_array_push(x_80, x_79);
|
||||
x_82 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_82 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_83 = lean_array_push(x_81, x_82);
|
||||
x_84 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_85 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -7729,7 +7729,7 @@ lean_ctor_set(x_123, 0, x_122);
|
|||
lean_ctor_set(x_123, 1, x_121);
|
||||
x_124 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_125 = lean_array_push(x_124, x_123);
|
||||
x_126 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_126 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_127 = lean_array_push(x_125, x_126);
|
||||
x_128 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_129 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
|
|||
4
stage0/stdlib/Lean/Elab/Do.c
generated
4
stage0/stdlib/Lean/Elab/Do.c
generated
|
|
@ -1017,7 +1017,6 @@ lean_object* l_Array_foldrMUnsafe_fold___at_Lean_Elab_Term_Do_attachJPs___spec__
|
|||
lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__34;
|
||||
uint8_t l_Array_anyMUnsafe_any___at_Lean_Elab_Term_Do_hasBreakContinueReturn___spec__2(lean_object*, size_t, size_t);
|
||||
lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_extractBind_match__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_Do_mkAuxDeclFor___rarg___lambda__3___closed__8;
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_Do_elabDo___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_Do_mkIte_match__1(lean_object*);
|
||||
|
|
@ -1123,6 +1122,7 @@ lean_object* l_Lean_Elab_Term_Do_getDoLetArrowVars___closed__2;
|
|||
lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTermCore___closed__12;
|
||||
lean_object* l_Lean_Elab_Term_Do_ToTerm_seqToTerm(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_foldrMUnsafe_fold___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkTuple___spec__2(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTermCore___closed__11;
|
||||
lean_object* l_Lean_throwError___at_Lean_Elab_Term_Do_mkJmp___spec__4___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_Do_ToTerm_continueToTermCore___closed__22;
|
||||
|
|
@ -18205,7 +18205,7 @@ x_9 = lean_nat_dec_eq(x_5, x_8);
|
|||
if (x_9 == 0)
|
||||
{
|
||||
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14;
|
||||
x_10 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_2);
|
||||
x_10 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_2);
|
||||
x_11 = lean_nat_sub(x_5, x_8);
|
||||
lean_dec(x_5);
|
||||
x_12 = l_Array_extract___rarg(x_2, x_6, x_11);
|
||||
|
|
|
|||
10
stage0/stdlib/Lean/Elab/Level.c
generated
10
stage0/stdlib/Lean/Elab/Level.c
generated
|
|
@ -99,7 +99,6 @@ lean_object* l_Lean_Elab_Level_instMonadRefLevelElabM___closed__2;
|
|||
lean_object* l_Lean_mkFreshId___at_Lean_Elab_Level_mkFreshLevelMVar___spec__1___rarg(lean_object*);
|
||||
lean_object* l_Lean_Elab_Level_instAddMessageContextLevelElabM___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Level_instMonadNameGeneratorLevelElabM___closed__1;
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(lean_object*);
|
||||
lean_object* l_Lean_throwError___at_Lean_Elab_Level_elabLevel___spec__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_string_length(lean_object*);
|
||||
lean_object* l_Lean_Elab_Level_instMonadRefLevelElabM___closed__1;
|
||||
|
|
@ -107,6 +106,7 @@ lean_object* l_Lean_Level_ofNat(lean_object*);
|
|||
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Level_elabLevel___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkLevelParam(lean_object*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
|
||||
lean_object* l_Lean_Elab_Level_instMonadNameGeneratorLevelElabM___closed__4;
|
||||
lean_object* l_Lean_Elab_Level_instMonadRefLevelElabM___closed__3;
|
||||
lean_object* l_Lean_Elab_Level_instMonadNameGeneratorLevelElabM___lambda__2(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -1449,7 +1449,7 @@ x_96 = l_Lean_Syntax_getArg(x_1, x_95);
|
|||
lean_dec(x_1);
|
||||
x_97 = l_Lean_Syntax_getArgs(x_96);
|
||||
lean_dec(x_96);
|
||||
x_98 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_97);
|
||||
x_98 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_97);
|
||||
lean_inc(x_2);
|
||||
x_99 = l_Lean_Elab_Level_elabLevel(x_98, x_2, x_3);
|
||||
if (lean_obj_tag(x_99) == 0)
|
||||
|
|
@ -1555,7 +1555,7 @@ x_124 = l_Lean_Syntax_getArg(x_1, x_123);
|
|||
lean_dec(x_1);
|
||||
x_125 = l_Lean_Syntax_getArgs(x_124);
|
||||
lean_dec(x_124);
|
||||
x_126 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_125);
|
||||
x_126 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_125);
|
||||
lean_inc(x_2);
|
||||
x_127 = l_Lean_Elab_Level_elabLevel(x_126, x_2, x_3);
|
||||
if (lean_obj_tag(x_127) == 0)
|
||||
|
|
@ -1987,7 +1987,7 @@ x_229 = l_Lean_Syntax_getArg(x_1, x_228);
|
|||
lean_dec(x_1);
|
||||
x_230 = l_Lean_Syntax_getArgs(x_229);
|
||||
lean_dec(x_229);
|
||||
x_231 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_230);
|
||||
x_231 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_230);
|
||||
lean_inc(x_157);
|
||||
x_232 = l_Lean_Elab_Level_elabLevel(x_231, x_157, x_3);
|
||||
if (lean_obj_tag(x_232) == 0)
|
||||
|
|
@ -2099,7 +2099,7 @@ x_257 = l_Lean_Syntax_getArg(x_1, x_256);
|
|||
lean_dec(x_1);
|
||||
x_258 = l_Lean_Syntax_getArgs(x_257);
|
||||
lean_dec(x_257);
|
||||
x_259 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_258);
|
||||
x_259 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_258);
|
||||
lean_inc(x_157);
|
||||
x_260 = l_Lean_Elab_Level_elabLevel(x_259, x_157, x_3);
|
||||
if (lean_obj_tag(x_260) == 0)
|
||||
|
|
|
|||
10
stage0/stdlib/Lean/Elab/Quotation.c
generated
10
stage0/stdlib/Lean/Elab/Quotation.c
generated
|
|
@ -455,7 +455,6 @@ lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_letBind
|
|||
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__4___closed__24;
|
||||
extern lean_object* l_Lean_Parser_Tactic_match___closed__3;
|
||||
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_floatOutAntiquotTerms___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
lean_object* l_List_redLength___rarg(lean_object*);
|
||||
lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_addTrace___at_Lean_Elab_Term_Quotation_match__syntax_expand___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -477,6 +476,7 @@ lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*);
|
|||
extern lean_object* l_Lean_Parser_Tactic_match___closed__5;
|
||||
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___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* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch_match__1(lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__18;
|
||||
lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__4___lambda__2___closed__6;
|
||||
lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__9___closed__17;
|
||||
|
|
@ -3394,7 +3394,7 @@ x_268 = lean_array_to_list(lean_box(0), x_107);
|
|||
x_269 = l___private_Init_Meta_0__Lean_quoteList___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__3(x_268);
|
||||
x_270 = l_Lean_mkOptionalNode___closed__2;
|
||||
x_271 = lean_array_push(x_270, x_269);
|
||||
x_272 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
x_272 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
x_273 = l_Lean_Syntax_mkCApp(x_272, x_271);
|
||||
x_274 = lean_array_push(x_267, x_273);
|
||||
x_275 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__4___closed__18;
|
||||
|
|
@ -4016,7 +4016,7 @@ x_535 = lean_array_to_list(lean_box(0), x_107);
|
|||
x_536 = l___private_Init_Meta_0__Lean_quoteList___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__3(x_535);
|
||||
x_537 = l_Lean_mkOptionalNode___closed__2;
|
||||
x_538 = lean_array_push(x_537, x_536);
|
||||
x_539 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
x_539 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
x_540 = l_Lean_Syntax_mkCApp(x_539, x_538);
|
||||
x_541 = lean_array_push(x_534, x_540);
|
||||
x_542 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__4___closed__18;
|
||||
|
|
@ -4868,7 +4868,7 @@ x_863 = lean_array_to_list(lean_box(0), x_699);
|
|||
x_864 = l___private_Init_Meta_0__Lean_quoteList___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__3(x_863);
|
||||
x_865 = l_Lean_mkOptionalNode___closed__2;
|
||||
x_866 = lean_array_push(x_865, x_864);
|
||||
x_867 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
x_867 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
x_868 = l_Lean_Syntax_mkCApp(x_867, x_866);
|
||||
x_869 = lean_array_push(x_862, x_868);
|
||||
x_870 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__4___closed__18;
|
||||
|
|
@ -5495,7 +5495,7 @@ x_1135 = lean_array_to_list(lean_box(0), x_699);
|
|||
x_1136 = l___private_Init_Meta_0__Lean_quoteList___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__3(x_1135);
|
||||
x_1137 = l_Lean_mkOptionalNode___closed__2;
|
||||
x_1138 = lean_array_push(x_1137, x_1136);
|
||||
x_1139 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
x_1139 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
x_1140 = l_Lean_Syntax_mkCApp(x_1139, x_1138);
|
||||
x_1141 = lean_array_push(x_1134, x_1140);
|
||||
x_1142 = l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___spec__4___closed__18;
|
||||
|
|
|
|||
138
stage0/stdlib/Lean/Elab/Syntax.c
generated
138
stage0/stdlib/Lean/Elab/Syntax.c
generated
|
|
@ -261,7 +261,6 @@ lean_object* l_Lean_Elab_Command_mkNameFromParserSyntax_visit(lean_object*, lean
|
|||
lean_object* l_Lean_Elab_Command_elabDeclareSyntaxCat___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed__2;
|
||||
extern lean_object* l_Lean_throwUnknownConstant___rarg___closed__2;
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
lean_object* l_Array_filterSepElemsM___at_Lean_Elab_Command_elabNoKindMacroRulesAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_declareSyntaxCatQuotParser___closed__4;
|
||||
lean_object* l_Lean_resolveGlobalName___at_Lean_Elab_Term_toParserDescrAux___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -284,6 +283,7 @@ uint8_t l_Lean_Parser_leadingIdentAsSymbol(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Elab_Term_toParserDescrAux___closed__53;
|
||||
lean_object* l_Lean_Elab_mkUnusedBaseName___at_Lean_Elab_Command_mkNameFromParserSyntax___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_string_utf8_next(lean_object*, lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
lean_object* l_Lean_throwError___at_Lean_Elab_Term_checkLeftRec___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_expandMixfix___closed__1;
|
||||
lean_object* l_Lean_Elab_Command_expandElab___closed__3;
|
||||
|
|
@ -838,6 +838,7 @@ extern lean_object* l_Lean_expandExplicitBindersAux_loop___closed__4;
|
|||
lean_object* l_Lean_Elab_Command_expandMixfix___lambda__1___closed__24;
|
||||
lean_object* l_Array_mapSepElemsM___at_Lean_Elab_Command_elabMacroRulesAux___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
lean_object* l_Lean_Elab_Command_expandMixfix___lambda__1___closed__20;
|
||||
lean_object* l_Lean_Elab_Command_elabSyntax_match__1(lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_expandMacroHeadIntoSyntaxItem(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -884,7 +885,6 @@ lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwErrorIfErrors___spec__1_
|
|||
lean_object* l_Lean_Elab_Command_inferMacroRulesAltKind___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Elab_Term_expandFunBinders_loop___closed__9;
|
||||
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Syntax_0__Lean_Elab_Command_expandNotationAux___spec__3___boxed(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
extern lean_object* l_Lean_Elab_toAttributeKind___rarg___lambda__2___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_toParserDescrAux_match__4___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Command_elabMacroRulesAux___closed__2;
|
||||
|
|
@ -10160,7 +10160,7 @@ lean_ctor_set(x_33, 0, x_32);
|
|||
lean_ctor_set(x_33, 1, x_31);
|
||||
x_34 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_35 = lean_array_push(x_34, x_33);
|
||||
x_36 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_36 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_37 = lean_array_push(x_35, x_36);
|
||||
x_38 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_39 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -12563,7 +12563,7 @@ lean_ctor_set(x_57, 0, x_51);
|
|||
lean_ctor_set(x_57, 1, x_56);
|
||||
x_58 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_59 = lean_array_push(x_58, x_57);
|
||||
x_60 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_60 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_61 = lean_array_push(x_59, x_60);
|
||||
x_62 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_63 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -12696,7 +12696,7 @@ lean_ctor_set(x_141, 0, x_135);
|
|||
lean_ctor_set(x_141, 1, x_140);
|
||||
x_142 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_143 = lean_array_push(x_142, x_141);
|
||||
x_144 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_144 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_145 = lean_array_push(x_143, x_144);
|
||||
x_146 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_147 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -12829,7 +12829,7 @@ lean_ctor_set(x_225, 0, x_219);
|
|||
lean_ctor_set(x_225, 1, x_224);
|
||||
x_226 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_227 = lean_array_push(x_226, x_225);
|
||||
x_228 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_228 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_229 = lean_array_push(x_227, x_228);
|
||||
x_230 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_231 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -12967,7 +12967,7 @@ lean_ctor_set(x_309, 0, x_303);
|
|||
lean_ctor_set(x_309, 1, x_308);
|
||||
x_310 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_311 = lean_array_push(x_310, x_309);
|
||||
x_312 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_312 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_313 = lean_array_push(x_311, x_312);
|
||||
x_314 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_315 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -13100,7 +13100,7 @@ lean_ctor_set(x_393, 0, x_387);
|
|||
lean_ctor_set(x_393, 1, x_392);
|
||||
x_394 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_395 = lean_array_push(x_394, x_393);
|
||||
x_396 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_396 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_397 = lean_array_push(x_395, x_396);
|
||||
x_398 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_399 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -13233,7 +13233,7 @@ lean_ctor_set(x_477, 0, x_471);
|
|||
lean_ctor_set(x_477, 1, x_476);
|
||||
x_478 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_479 = lean_array_push(x_478, x_477);
|
||||
x_480 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_480 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_481 = lean_array_push(x_479, x_480);
|
||||
x_482 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_483 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -15138,7 +15138,7 @@ lean_ctor_set(x_33, 0, x_27);
|
|||
lean_ctor_set(x_33, 1, x_32);
|
||||
x_34 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_35 = lean_array_push(x_34, x_33);
|
||||
x_36 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_36 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_37 = lean_array_push(x_35, x_36);
|
||||
x_38 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_39 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -15321,7 +15321,7 @@ lean_ctor_set(x_140, 0, x_134);
|
|||
lean_ctor_set(x_140, 1, x_139);
|
||||
x_141 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_142 = lean_array_push(x_141, x_140);
|
||||
x_143 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_143 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_144 = lean_array_push(x_142, x_143);
|
||||
x_145 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_146 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -17545,9 +17545,9 @@ lean_ctor_set(x_77, 0, x_15);
|
|||
lean_ctor_set(x_77, 1, x_76);
|
||||
x_78 = l_Lean_Elab_Command_expandMixfix___lambda__1___closed__20;
|
||||
x_79 = lean_array_push(x_78, x_77);
|
||||
x_80 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_80 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_81 = lean_array_push(x_80, x_65);
|
||||
x_82 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_82 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_83 = lean_array_push(x_81, x_82);
|
||||
x_84 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_84, 0, x_15);
|
||||
|
|
@ -17838,9 +17838,9 @@ lean_ctor_set(x_199, 1, x_198);
|
|||
x_200 = l_Lean_Elab_Command_expandMixfix___lambda__1___closed__20;
|
||||
lean_inc(x_199);
|
||||
x_201 = lean_array_push(x_200, x_199);
|
||||
x_202 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_202 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_203 = lean_array_push(x_202, x_187);
|
||||
x_204 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_204 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_205 = lean_array_push(x_203, x_204);
|
||||
x_206 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_206, 0, x_15);
|
||||
|
|
@ -18167,9 +18167,9 @@ lean_ctor_set(x_326, 0, x_15);
|
|||
lean_ctor_set(x_326, 1, x_325);
|
||||
x_327 = l_Lean_Elab_Command_expandMixfix___lambda__1___closed__20;
|
||||
x_328 = lean_array_push(x_327, x_326);
|
||||
x_329 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_329 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_330 = lean_array_push(x_329, x_308);
|
||||
x_331 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_331 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_332 = lean_array_push(x_330, x_331);
|
||||
x_333 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_333, 0, x_15);
|
||||
|
|
@ -18503,9 +18503,9 @@ lean_ctor_set(x_478, 1, x_477);
|
|||
x_479 = l_Lean_Elab_Command_expandMixfix___lambda__1___closed__20;
|
||||
lean_inc(x_478);
|
||||
x_480 = lean_array_push(x_479, x_478);
|
||||
x_481 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_481 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_482 = lean_array_push(x_481, x_466);
|
||||
x_483 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_483 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_484 = lean_array_push(x_482, x_483);
|
||||
x_485 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_485, 0, x_15);
|
||||
|
|
@ -18766,9 +18766,9 @@ lean_ctor_set(x_616, 0, x_15);
|
|||
lean_ctor_set(x_616, 1, x_615);
|
||||
x_617 = l_Lean_Elab_Command_expandMixfix___lambda__1___closed__38;
|
||||
x_618 = lean_array_push(x_617, x_616);
|
||||
x_619 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_619 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_620 = lean_array_push(x_619, x_606);
|
||||
x_621 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_621 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_622 = lean_array_push(x_620, x_621);
|
||||
x_623 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_623, 0, x_15);
|
||||
|
|
@ -20069,7 +20069,7 @@ lean_ctor_set(x_63, 0, x_36);
|
|||
lean_ctor_set(x_63, 1, x_62);
|
||||
x_64 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_65 = lean_array_push(x_64, x_63);
|
||||
x_66 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_66 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_67 = lean_array_push(x_65, x_66);
|
||||
x_68 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_69 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -20259,7 +20259,7 @@ lean_ctor_set(x_177, 0, x_36);
|
|||
lean_ctor_set(x_177, 1, x_176);
|
||||
x_178 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_179 = lean_array_push(x_178, x_177);
|
||||
x_180 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_180 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_181 = lean_array_push(x_179, x_180);
|
||||
x_182 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_183 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -20500,7 +20500,7 @@ lean_ctor_set(x_311, 0, x_284);
|
|||
lean_ctor_set(x_311, 1, x_310);
|
||||
x_312 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_313 = lean_array_push(x_312, x_311);
|
||||
x_314 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_314 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_315 = lean_array_push(x_313, x_314);
|
||||
x_316 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_317 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -20690,7 +20690,7 @@ lean_ctor_set(x_425, 0, x_284);
|
|||
lean_ctor_set(x_425, 1, x_424);
|
||||
x_426 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_427 = lean_array_push(x_426, x_425);
|
||||
x_428 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_428 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_429 = lean_array_push(x_427, x_428);
|
||||
x_430 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_431 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -20933,7 +20933,7 @@ lean_ctor_set(x_561, 0, x_534);
|
|||
lean_ctor_set(x_561, 1, x_560);
|
||||
x_562 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_563 = lean_array_push(x_562, x_561);
|
||||
x_564 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_564 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_565 = lean_array_push(x_563, x_564);
|
||||
x_566 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_567 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -21123,7 +21123,7 @@ lean_ctor_set(x_675, 0, x_534);
|
|||
lean_ctor_set(x_675, 1, x_674);
|
||||
x_676 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_677 = lean_array_push(x_676, x_675);
|
||||
x_678 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_678 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_679 = lean_array_push(x_677, x_678);
|
||||
x_680 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_681 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -21393,7 +21393,7 @@ lean_ctor_set(x_816, 0, x_788);
|
|||
lean_ctor_set(x_816, 1, x_815);
|
||||
x_817 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_818 = lean_array_push(x_817, x_816);
|
||||
x_819 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_819 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_820 = lean_array_push(x_818, x_819);
|
||||
x_821 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_822 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -21645,7 +21645,7 @@ lean_ctor_set(x_952, 0, x_924);
|
|||
lean_ctor_set(x_952, 1, x_951);
|
||||
x_953 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_954 = lean_array_push(x_953, x_952);
|
||||
x_955 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_955 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_956 = lean_array_push(x_954, x_955);
|
||||
x_957 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_958 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -21899,7 +21899,7 @@ lean_ctor_set(x_1090, 0, x_1062);
|
|||
lean_ctor_set(x_1090, 1, x_1089);
|
||||
x_1091 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_1092 = lean_array_push(x_1091, x_1090);
|
||||
x_1093 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_1093 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_1094 = lean_array_push(x_1092, x_1093);
|
||||
x_1095 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_1096 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -22293,7 +22293,7 @@ lean_ctor_set(x_1253, 0, x_1225);
|
|||
lean_ctor_set(x_1253, 1, x_1252);
|
||||
x_1254 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_1255 = lean_array_push(x_1254, x_1253);
|
||||
x_1256 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_1256 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_1257 = lean_array_push(x_1255, x_1256);
|
||||
x_1258 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_1259 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -22550,7 +22550,7 @@ lean_ctor_set(x_1390, 0, x_1362);
|
|||
lean_ctor_set(x_1390, 1, x_1389);
|
||||
x_1391 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_1392 = lean_array_push(x_1391, x_1390);
|
||||
x_1393 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_1393 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_1394 = lean_array_push(x_1392, x_1393);
|
||||
x_1395 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_1396 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -22809,7 +22809,7 @@ lean_ctor_set(x_1529, 0, x_1501);
|
|||
lean_ctor_set(x_1529, 1, x_1528);
|
||||
x_1530 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__13;
|
||||
x_1531 = lean_array_push(x_1530, x_1529);
|
||||
x_1532 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_1532 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_1533 = lean_array_push(x_1531, x_1532);
|
||||
x_1534 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__10;
|
||||
x_1535 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -23929,9 +23929,9 @@ x_61 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed__
|
|||
x_62 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_62, 0, x_61);
|
||||
lean_ctor_set(x_62, 1, x_60);
|
||||
x_63 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_63 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_64 = lean_array_push(x_63, x_62);
|
||||
x_65 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_65 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_66 = lean_array_push(x_64, x_65);
|
||||
x_67 = l_Lean_nullKind___closed__2;
|
||||
x_68 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -23982,9 +23982,9 @@ x_94 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed__
|
|||
x_95 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_95, 0, x_94);
|
||||
lean_ctor_set(x_95, 1, x_93);
|
||||
x_96 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_96 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_97 = lean_array_push(x_96, x_95);
|
||||
x_98 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_98 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_99 = lean_array_push(x_97, x_98);
|
||||
x_100 = l_Lean_nullKind___closed__2;
|
||||
x_101 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -24035,9 +24035,9 @@ x_127 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed_
|
|||
x_128 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_128, 0, x_127);
|
||||
lean_ctor_set(x_128, 1, x_126);
|
||||
x_129 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_129 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_130 = lean_array_push(x_129, x_128);
|
||||
x_131 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_131 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_132 = lean_array_push(x_130, x_131);
|
||||
x_133 = l_Lean_nullKind___closed__2;
|
||||
x_134 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -24109,9 +24109,9 @@ x_170 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed_
|
|||
x_171 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_171, 0, x_170);
|
||||
lean_ctor_set(x_171, 1, x_169);
|
||||
x_172 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_172 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_173 = lean_array_push(x_172, x_171);
|
||||
x_174 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_174 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_175 = lean_array_push(x_173, x_174);
|
||||
x_176 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_176, 0, x_157);
|
||||
|
|
@ -24176,9 +24176,9 @@ x_211 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed_
|
|||
x_212 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_212, 0, x_211);
|
||||
lean_ctor_set(x_212, 1, x_210);
|
||||
x_213 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_213 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_214 = lean_array_push(x_213, x_212);
|
||||
x_215 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_215 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_216 = lean_array_push(x_214, x_215);
|
||||
x_217 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_217, 0, x_198);
|
||||
|
|
@ -24243,9 +24243,9 @@ x_252 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed_
|
|||
x_253 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_253, 0, x_252);
|
||||
lean_ctor_set(x_253, 1, x_251);
|
||||
x_254 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_254 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_255 = lean_array_push(x_254, x_253);
|
||||
x_256 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_256 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_257 = lean_array_push(x_255, x_256);
|
||||
x_258 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_258, 0, x_239);
|
||||
|
|
@ -26222,9 +26222,9 @@ x_65 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed__
|
|||
x_66 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_66, 0, x_65);
|
||||
lean_ctor_set(x_66, 1, x_64);
|
||||
x_67 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_67 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_68 = lean_array_push(x_67, x_66);
|
||||
x_69 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_69 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_70 = lean_array_push(x_68, x_69);
|
||||
x_71 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_71, 0, x_52);
|
||||
|
|
@ -26320,9 +26320,9 @@ x_127 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed_
|
|||
x_128 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_128, 0, x_127);
|
||||
lean_ctor_set(x_128, 1, x_126);
|
||||
x_129 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_129 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_130 = lean_array_push(x_129, x_128);
|
||||
x_131 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_131 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_132 = lean_array_push(x_130, x_131);
|
||||
x_133 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_133, 0, x_114);
|
||||
|
|
@ -26432,9 +26432,9 @@ x_196 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed_
|
|||
x_197 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_197, 0, x_196);
|
||||
lean_ctor_set(x_197, 1, x_195);
|
||||
x_198 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_198 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_199 = lean_array_push(x_198, x_197);
|
||||
x_200 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_200 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_201 = lean_array_push(x_199, x_200);
|
||||
x_202 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_202, 0, x_183);
|
||||
|
|
@ -26525,9 +26525,9 @@ x_255 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed_
|
|||
x_256 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_256, 0, x_255);
|
||||
lean_ctor_set(x_256, 1, x_254);
|
||||
x_257 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_257 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_258 = lean_array_push(x_257, x_256);
|
||||
x_259 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_259 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_260 = lean_array_push(x_258, x_259);
|
||||
x_261 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_261, 0, x_242);
|
||||
|
|
@ -28341,9 +28341,9 @@ x_78 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed__
|
|||
x_79 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_79, 0, x_78);
|
||||
lean_ctor_set(x_79, 1, x_77);
|
||||
x_80 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_80 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_81 = lean_array_push(x_80, x_79);
|
||||
x_82 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_82 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_83 = lean_array_push(x_81, x_82);
|
||||
x_84 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_84, 0, x_66);
|
||||
|
|
@ -28562,9 +28562,9 @@ x_213 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed_
|
|||
x_214 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_214, 0, x_213);
|
||||
lean_ctor_set(x_214, 1, x_212);
|
||||
x_215 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_215 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_216 = lean_array_push(x_215, x_214);
|
||||
x_217 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_217 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_218 = lean_array_push(x_216, x_217);
|
||||
x_219 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_219, 0, x_201);
|
||||
|
|
@ -28796,9 +28796,9 @@ x_353 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed_
|
|||
x_354 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_354, 0, x_353);
|
||||
lean_ctor_set(x_354, 1, x_352);
|
||||
x_355 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_355 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_356 = lean_array_push(x_355, x_354);
|
||||
x_357 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_357 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_358 = lean_array_push(x_356, x_357);
|
||||
x_359 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_359, 0, x_341);
|
||||
|
|
@ -29018,9 +29018,9 @@ x_489 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed_
|
|||
x_490 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_490, 0, x_489);
|
||||
lean_ctor_set(x_490, 1, x_488);
|
||||
x_491 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_491 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_492 = lean_array_push(x_491, x_490);
|
||||
x_493 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_493 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_494 = lean_array_push(x_492, x_493);
|
||||
x_495 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_495, 0, x_477);
|
||||
|
|
@ -29253,9 +29253,9 @@ x_630 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed_
|
|||
x_631 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_631, 0, x_630);
|
||||
lean_ctor_set(x_631, 1, x_629);
|
||||
x_632 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_632 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_633 = lean_array_push(x_632, x_631);
|
||||
x_634 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_634 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_635 = lean_array_push(x_633, x_634);
|
||||
x_636 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_636, 0, x_618);
|
||||
|
|
@ -29518,9 +29518,9 @@ x_792 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed_
|
|||
x_793 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_793, 0, x_792);
|
||||
lean_ctor_set(x_793, 1, x_791);
|
||||
x_794 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_794 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_795 = lean_array_push(x_794, x_793);
|
||||
x_796 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_796 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_797 = lean_array_push(x_795, x_796);
|
||||
x_798 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_798, 0, x_780);
|
||||
|
|
@ -29827,9 +29827,9 @@ x_968 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed_
|
|||
x_969 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_969, 0, x_968);
|
||||
lean_ctor_set(x_969, 1, x_967);
|
||||
x_970 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_970 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_971 = lean_array_push(x_970, x_969);
|
||||
x_972 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_972 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_973 = lean_array_push(x_971, x_972);
|
||||
x_974 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_974, 0, x_956);
|
||||
|
|
@ -30138,9 +30138,9 @@ x_1153 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Command_elabKindPrio___closed
|
|||
x_1154 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_1154, 0, x_1153);
|
||||
lean_ctor_set(x_1154, 1, x_1152);
|
||||
x_1155 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_1155 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_1156 = lean_array_push(x_1155, x_1154);
|
||||
x_1157 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_1157 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_1158 = lean_array_push(x_1156, x_1157);
|
||||
x_1159 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_1159, 0, x_1141);
|
||||
|
|
|
|||
6
stage0/stdlib/Lean/Meta/AppBuilder.c
generated
6
stage0/stdlib/Lean/Meta/AppBuilder.c
generated
|
|
@ -312,7 +312,6 @@ lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkCongrFunImp___close
|
|||
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___lambda__1___closed__2;
|
||||
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppOptMAux_match__3___rarg(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Syntax_mkApp___closed__1;
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
lean_object* l_Lean_Meta_mkAppM_match__1___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_mkEqTrans___rarg(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -320,6 +319,7 @@ lean_object* l_Lean_setEnv___at_Lean_Meta_setInlineAttribute___spec__1(lean_obje
|
|||
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___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* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkCongrImp_match__1(lean_object*);
|
||||
lean_object* l_List_map___at_Lean_MessageData_instCoeListExprMessageData___spec__1(lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkProjectionImp_match__5___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkCongrArgImp_match__1(lean_object*);
|
||||
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
|
||||
|
|
@ -10981,7 +10981,7 @@ x_12 = lean_box(0);
|
|||
x_13 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_13, 0, x_3);
|
||||
lean_ctor_set(x_13, 1, x_12);
|
||||
x_14 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
x_14 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
x_15 = l_Lean_mkConst(x_14, x_13);
|
||||
x_16 = l_Lean_mkApp(x_15, x_1);
|
||||
x_17 = l_Lean_mkApp(x_16, x_11);
|
||||
|
|
@ -11000,7 +11000,7 @@ x_20 = lean_box(0);
|
|||
x_21 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_21, 0, x_3);
|
||||
lean_ctor_set(x_21, 1, x_20);
|
||||
x_22 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
x_22 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
x_23 = l_Lean_mkConst(x_22, x_21);
|
||||
x_24 = l_Lean_mkApp(x_23, x_1);
|
||||
x_25 = l_Lean_mkApp(x_24, x_18);
|
||||
|
|
|
|||
6
stage0/stdlib/Lean/Meta/Match/CaseArraySizes.c
generated
6
stage0/stdlib/Lean/Meta/Match/CaseArraySizes.c
generated
|
|
@ -95,11 +95,11 @@ lean_object* l_Lean_Meta_FVarSubst_get(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Meta_getArrayArgType___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Syntax_mkApp___closed__1;
|
||||
lean_object* l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_introArrayLit_loop___closed__2;
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
lean_object* l_Lean_Meta_assertExt(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_caseArraySizes_match__6(lean_object*);
|
||||
lean_object* l_Lean_Meta_instInhabitedCaseArraySizesSubgoal___closed__1;
|
||||
lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_caseArraySizes___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_caseArraySizes_match__2(lean_object*);
|
||||
extern lean_object* l_Std_PersistentHashMap_mkCollisionNode___rarg___closed__1;
|
||||
|
|
@ -728,7 +728,7 @@ x_14 = lean_box(0);
|
|||
x_15 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_15, 0, x_9);
|
||||
lean_ctor_set(x_15, 1, x_14);
|
||||
x_16 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
x_16 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
x_17 = l_Lean_mkConst(x_16, x_15);
|
||||
x_18 = l_Lean_mkApp(x_17, x_1);
|
||||
x_19 = l_Lean_mkApp(x_18, x_13);
|
||||
|
|
@ -747,7 +747,7 @@ x_22 = lean_box(0);
|
|||
x_23 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_23, 0, x_9);
|
||||
lean_ctor_set(x_23, 1, x_22);
|
||||
x_24 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
x_24 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
x_25 = l_Lean_mkConst(x_24, x_23);
|
||||
x_26 = l_Lean_mkApp(x_25, x_1);
|
||||
x_27 = l_Lean_mkApp(x_26, x_20);
|
||||
|
|
|
|||
54
stage0/stdlib/Lean/Parser/Basic.c
generated
54
stage0/stdlib/Lean/Parser/Basic.c
generated
|
|
@ -799,7 +799,6 @@ uint8_t l_Lean_isIdFirst(uint32_t);
|
|||
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_takeWhile1Fn(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_instInhabitedParserFn___rarg___boxed(lean_object*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(lean_object*);
|
||||
lean_object* l_Lean_Parser_errorFn___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_identEqFn_match__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_many1Unbox(lean_object*);
|
||||
|
|
@ -884,6 +883,7 @@ lean_object* l_Lean_Parser_ParserState_mkEOIError(lean_object*);
|
|||
lean_object* l_Lean_Parser_checkLineEqFn_match__1(lean_object*);
|
||||
lean_object* l_Lean_Parser_unicodeSymbolFnAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_EnvExtensionInterfaceUnsafe_getState___rarg(lean_object*, lean_object*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
|
||||
lean_object* l_Lean_Parser_indexed___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_rawFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_categoryParserOfStackFn(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -4686,7 +4686,7 @@ _start:
|
|||
lean_object* x_5; lean_object* x_6; lean_object* x_7; uint8_t x_8;
|
||||
x_5 = lean_ctor_get(x_4, 0);
|
||||
lean_inc(x_5);
|
||||
x_6 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_5);
|
||||
x_6 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_5);
|
||||
lean_dec(x_5);
|
||||
x_7 = lean_apply_1(x_1, x_6);
|
||||
x_8 = lean_unbox(x_7);
|
||||
|
|
@ -7392,7 +7392,7 @@ if (lean_obj_tag(x_6) == 0)
|
|||
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
|
||||
x_7 = lean_ctor_get(x_5, 0);
|
||||
lean_inc(x_7);
|
||||
x_8 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_7);
|
||||
x_8 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_7);
|
||||
lean_dec(x_7);
|
||||
x_9 = l_Lean_Parser_ParserState_popSyntax(x_5);
|
||||
x_10 = lean_apply_1(x_2, x_8);
|
||||
|
|
@ -10372,7 +10372,7 @@ lean_object* x_11; lean_object* x_12;
|
|||
lean_dec(x_1);
|
||||
x_11 = lean_ctor_get(x_9, 0);
|
||||
lean_inc(x_11);
|
||||
x_12 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_11);
|
||||
x_12 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_11);
|
||||
lean_dec(x_11);
|
||||
if (lean_obj_tag(x_12) == 3)
|
||||
{
|
||||
|
|
@ -10615,7 +10615,7 @@ x_12 = lean_ctor_get(x_2, 1);
|
|||
lean_dec(x_12);
|
||||
x_13 = lean_ctor_get(x_2, 0);
|
||||
lean_dec(x_13);
|
||||
x_14 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_4);
|
||||
x_14 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_4);
|
||||
lean_inc(x_5);
|
||||
x_15 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_15, 0, x_1);
|
||||
|
|
@ -10630,7 +10630,7 @@ else
|
|||
{
|
||||
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
|
||||
lean_dec(x_2);
|
||||
x_17 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_4);
|
||||
x_17 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_4);
|
||||
lean_inc(x_5);
|
||||
x_18 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_18, 0, x_1);
|
||||
|
|
@ -10735,7 +10735,7 @@ if (lean_obj_tag(x_7) == 0)
|
|||
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
|
||||
x_8 = lean_ctor_get(x_6, 0);
|
||||
lean_inc(x_8);
|
||||
x_9 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_8);
|
||||
x_9 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_8);
|
||||
lean_dec(x_8);
|
||||
x_10 = l_Lean_Parser_ParserState_restore(x_6, x_4, x_5);
|
||||
lean_dec(x_4);
|
||||
|
|
@ -10874,7 +10874,7 @@ if (lean_obj_tag(x_7) == 0)
|
|||
lean_object* x_8; lean_object* x_9;
|
||||
x_8 = lean_ctor_get(x_6, 0);
|
||||
lean_inc(x_8);
|
||||
x_9 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_8);
|
||||
x_9 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_8);
|
||||
lean_dec(x_8);
|
||||
if (lean_obj_tag(x_9) == 2)
|
||||
{
|
||||
|
|
@ -10935,7 +10935,7 @@ if (lean_obj_tag(x_9) == 0)
|
|||
lean_object* x_10; lean_object* x_11;
|
||||
x_10 = lean_ctor_get(x_8, 0);
|
||||
lean_inc(x_10);
|
||||
x_11 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_10);
|
||||
x_11 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_10);
|
||||
lean_dec(x_10);
|
||||
if (lean_obj_tag(x_11) == 2)
|
||||
{
|
||||
|
|
@ -11150,7 +11150,7 @@ if (lean_obj_tag(x_7) == 0)
|
|||
lean_object* x_8; lean_object* x_9;
|
||||
x_8 = lean_ctor_get(x_6, 0);
|
||||
lean_inc(x_8);
|
||||
x_9 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_8);
|
||||
x_9 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_8);
|
||||
lean_dec(x_8);
|
||||
switch (lean_obj_tag(x_9)) {
|
||||
case 2:
|
||||
|
|
@ -11580,7 +11580,7 @@ _start:
|
|||
lean_object* x_4; lean_object* x_5; uint8_t x_6;
|
||||
x_4 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_4);
|
||||
x_5 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_4);
|
||||
x_5 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_4);
|
||||
lean_dec(x_4);
|
||||
x_6 = l_Lean_Parser_checkTailWs(x_5);
|
||||
lean_dec(x_5);
|
||||
|
|
@ -11929,7 +11929,7 @@ if (lean_obj_tag(x_8) == 0)
|
|||
lean_object* x_9; lean_object* x_10;
|
||||
x_9 = lean_ctor_get(x_7, 0);
|
||||
lean_inc(x_9);
|
||||
x_10 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_9);
|
||||
x_10 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_9);
|
||||
lean_dec(x_9);
|
||||
if (lean_obj_tag(x_10) == 2)
|
||||
{
|
||||
|
|
@ -12199,7 +12199,7 @@ if (lean_obj_tag(x_5) == 0)
|
|||
lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9;
|
||||
x_6 = lean_ctor_get(x_4, 0);
|
||||
lean_inc(x_6);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_6);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_6);
|
||||
lean_dec(x_6);
|
||||
x_8 = l_Lean_numLitKind;
|
||||
x_9 = l_Lean_Syntax_isOfKind(x_7, x_8);
|
||||
|
|
@ -12285,7 +12285,7 @@ if (lean_obj_tag(x_5) == 0)
|
|||
lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9;
|
||||
x_6 = lean_ctor_get(x_4, 0);
|
||||
lean_inc(x_6);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_6);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_6);
|
||||
lean_dec(x_6);
|
||||
x_8 = l_Lean_scientificLitKind;
|
||||
x_9 = l_Lean_Syntax_isOfKind(x_7, x_8);
|
||||
|
|
@ -12371,7 +12371,7 @@ if (lean_obj_tag(x_5) == 0)
|
|||
lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9;
|
||||
x_6 = lean_ctor_get(x_4, 0);
|
||||
lean_inc(x_6);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_6);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_6);
|
||||
lean_dec(x_6);
|
||||
x_8 = l_Lean_strLitKind;
|
||||
x_9 = l_Lean_Syntax_isOfKind(x_7, x_8);
|
||||
|
|
@ -12457,7 +12457,7 @@ if (lean_obj_tag(x_5) == 0)
|
|||
lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9;
|
||||
x_6 = lean_ctor_get(x_4, 0);
|
||||
lean_inc(x_6);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_6);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_6);
|
||||
lean_dec(x_6);
|
||||
x_8 = l_Lean_charLitKind;
|
||||
x_9 = l_Lean_Syntax_isOfKind(x_7, x_8);
|
||||
|
|
@ -12543,7 +12543,7 @@ if (lean_obj_tag(x_5) == 0)
|
|||
lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9;
|
||||
x_6 = lean_ctor_get(x_4, 0);
|
||||
lean_inc(x_6);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_6);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_6);
|
||||
lean_dec(x_6);
|
||||
x_8 = l_Lean_nameLitKind;
|
||||
x_9 = l_Lean_Syntax_isOfKind(x_7, x_8);
|
||||
|
|
@ -12629,7 +12629,7 @@ if (lean_obj_tag(x_5) == 0)
|
|||
lean_object* x_6; lean_object* x_7; uint8_t x_8;
|
||||
x_6 = lean_ctor_get(x_4, 0);
|
||||
lean_inc(x_6);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_6);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_6);
|
||||
lean_dec(x_6);
|
||||
x_8 = l_Lean_Syntax_isIdent(x_7);
|
||||
lean_dec(x_7);
|
||||
|
|
@ -12779,7 +12779,7 @@ if (lean_obj_tag(x_6) == 0)
|
|||
lean_object* x_7; lean_object* x_8;
|
||||
x_7 = lean_ctor_get(x_5, 0);
|
||||
lean_inc(x_7);
|
||||
x_8 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_7);
|
||||
x_8 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_7);
|
||||
lean_dec(x_7);
|
||||
if (lean_obj_tag(x_8) == 3)
|
||||
{
|
||||
|
|
@ -13213,7 +13213,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_obj
|
|||
x_4 = lean_ctor_get(x_1, 0);
|
||||
x_5 = lean_ctor_get(x_1, 3);
|
||||
lean_dec(x_5);
|
||||
x_6 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_4);
|
||||
x_6 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_4);
|
||||
x_7 = l_Array_shrink___rarg(x_4, x_2);
|
||||
x_8 = lean_array_push(x_7, x_6);
|
||||
x_9 = lean_box(0);
|
||||
|
|
@ -13231,7 +13231,7 @@ lean_inc(x_12);
|
|||
lean_inc(x_11);
|
||||
lean_inc(x_10);
|
||||
lean_dec(x_1);
|
||||
x_13 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_10);
|
||||
x_13 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_10);
|
||||
x_14 = l_Array_shrink___rarg(x_10, x_2);
|
||||
x_15 = lean_array_push(x_14, x_13);
|
||||
x_16 = lean_box(0);
|
||||
|
|
@ -13397,7 +13397,7 @@ return x_26;
|
|||
else
|
||||
{
|
||||
lean_object* x_27; lean_object* x_28; lean_object* x_29;
|
||||
x_27 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_20);
|
||||
x_27 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_20);
|
||||
lean_dec(x_20);
|
||||
x_28 = l_Lean_Parser_ParserState_shrinkStack(x_18, x_6);
|
||||
lean_dec(x_6);
|
||||
|
|
@ -13643,7 +13643,7 @@ lean_dec(x_9);
|
|||
lean_dec(x_4);
|
||||
x_40 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_40);
|
||||
x_41 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_40);
|
||||
x_41 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_40);
|
||||
lean_dec(x_40);
|
||||
x_42 = l_Lean_Parser_ParserState_shrinkStack(x_14, x_2);
|
||||
x_43 = l_Lean_Parser_ParserState_pushSyntax(x_42, x_41);
|
||||
|
|
@ -26817,7 +26817,7 @@ _start:
|
|||
lean_object* x_3; lean_object* x_4; uint8_t x_5;
|
||||
x_3 = lean_ctor_get(x_2, 0);
|
||||
lean_inc(x_3);
|
||||
x_4 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_3);
|
||||
x_4 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_3);
|
||||
lean_dec(x_3);
|
||||
x_5 = l_Lean_Parser_checkTailNoWs(x_4);
|
||||
lean_dec(x_4);
|
||||
|
|
@ -29463,7 +29463,7 @@ lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_obj
|
|||
x_3 = l___private_Lean_Parser_Basic_0__Lean_Parser_mkResult(x_1, x_2);
|
||||
x_4 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_4);
|
||||
x_5 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_4);
|
||||
x_5 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_4);
|
||||
lean_dec(x_4);
|
||||
x_6 = l_Lean_Parser_ParserState_popSyntax(x_3);
|
||||
x_7 = l_Lean_Parser_ParserState_popSyntax(x_6);
|
||||
|
|
@ -29513,7 +29513,7 @@ if (x_9 == 0)
|
|||
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
|
||||
x_10 = lean_ctor_get(x_7, 0);
|
||||
lean_inc(x_10);
|
||||
x_11 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_10);
|
||||
x_11 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_10);
|
||||
x_12 = lean_array_get_size(x_10);
|
||||
lean_dec(x_10);
|
||||
x_13 = lean_ctor_get(x_7, 1);
|
||||
|
|
@ -29568,7 +29568,7 @@ if (x_22 == 0)
|
|||
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
|
||||
x_23 = lean_ctor_get(x_7, 0);
|
||||
lean_inc(x_23);
|
||||
x_24 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_23);
|
||||
x_24 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_23);
|
||||
x_25 = lean_array_get_size(x_23);
|
||||
lean_dec(x_23);
|
||||
x_26 = lean_ctor_get(x_7, 1);
|
||||
|
|
|
|||
4
stage0/stdlib/Lean/Parser/Extension.c
generated
4
stage0/stdlib/Lean/Parser/Extension.c
generated
|
|
@ -496,7 +496,6 @@ lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_ob
|
|||
lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_throwParserCategoryAlreadyDefined___rarg___closed__1;
|
||||
lean_object* l_Lean_Parser_mkParserOfConstant(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_addTrailingParserAux(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(lean_object*);
|
||||
lean_object* lean_io_initializing(lean_object*);
|
||||
lean_object* l_Lean_Parser_getConstAlias___rarg___closed__3;
|
||||
lean_object* l_Lean_ScopedEnvExtension_add___at___private_Lean_Parser_Extension_0__Lean_Parser_ParserAttribute_add___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -537,6 +536,7 @@ lean_object* l_Lean_registerAttributeImplBuilder(lean_object*, lean_object*, lea
|
|||
lean_object* l_Lean_Parser_ParserState_mkUnexpectedError(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_3652____closed__2;
|
||||
lean_object* l_Lean_Parser_getSyntaxNodeKinds___boxed(lean_object*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
|
||||
lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_ParserExtension_OLeanEntry_toEntry_match__2(lean_object*);
|
||||
lean_object* l_IO_ofExcept___at_Lean_KeyedDeclsAttribute_declareBuiltin___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Std_PersistentHashMap_containsAux___at_Lean_Parser_isValidSyntaxNodeKind___spec__2___boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -10099,7 +10099,7 @@ lean_dec(x_9);
|
|||
x_20 = lean_ctor_get(x_12, 0);
|
||||
lean_inc(x_20);
|
||||
lean_dec(x_12);
|
||||
x_21 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_20);
|
||||
x_21 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_20);
|
||||
lean_dec(x_20);
|
||||
x_22 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_22, 0, x_21);
|
||||
|
|
|
|||
10
stage0/stdlib/Lean/Parser/Module.c
generated
10
stage0/stdlib/Lean/Parser/Module.c
generated
|
|
@ -275,7 +275,6 @@ uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Parser_Module_import___closed__5;
|
||||
lean_object* l_Lean_Parser_Module_module_parenthesizer___closed__3;
|
||||
lean_object* l_Lean_Parser_Module_header_formatter___closed__3;
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(lean_object*);
|
||||
lean_object* l_Lean_Parser_errorFn___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Module_module___elambda__1___closed__7;
|
||||
lean_object* l_Lean_Parser_Module_prelude___elambda__1(lean_object*, lean_object*);
|
||||
|
|
@ -302,6 +301,7 @@ lean_object* l_Lean_Parser_Module_import_formatter___closed__1;
|
|||
extern lean_object* l_Lean_initFn____x40_Lean_Parser_Extra___hyg_1069____closed__11;
|
||||
lean_object* l_Lean_Message_toString(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Module_prelude___elambda__1___closed__8;
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
|
||||
lean_object* l_Lean_Parser_Module_import___elambda__1___closed__3;
|
||||
lean_object* l_Lean_Parser_Module_updateTokens_match__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Module_header_formatter___closed__10;
|
||||
|
|
@ -2419,7 +2419,7 @@ lean_inc(x_11);
|
|||
x_16 = l_Lean_Parser_Module_header___elambda__1(x_11, x_15);
|
||||
x_17 = lean_ctor_get(x_16, 0);
|
||||
lean_inc(x_17);
|
||||
x_18 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_17);
|
||||
x_18 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_17);
|
||||
lean_dec(x_17);
|
||||
x_19 = lean_ctor_get(x_16, 3);
|
||||
lean_inc(x_19);
|
||||
|
|
@ -2501,7 +2501,7 @@ lean_inc(x_42);
|
|||
x_47 = l_Lean_Parser_Module_header___elambda__1(x_42, x_46);
|
||||
x_48 = lean_ctor_get(x_47, 0);
|
||||
lean_inc(x_48);
|
||||
x_49 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_48);
|
||||
x_49 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_48);
|
||||
lean_dec(x_48);
|
||||
x_50 = lean_ctor_get(x_47, 3);
|
||||
lean_inc(x_50);
|
||||
|
|
@ -2886,7 +2886,7 @@ lean_dec(x_2);
|
|||
lean_dec(x_1);
|
||||
x_19 = lean_ctor_get(x_17, 0);
|
||||
lean_inc(x_19);
|
||||
x_20 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_19);
|
||||
x_20 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_19);
|
||||
lean_dec(x_19);
|
||||
x_21 = lean_ctor_get(x_17, 1);
|
||||
lean_inc(x_21);
|
||||
|
|
@ -3004,7 +3004,7 @@ lean_dec(x_2);
|
|||
lean_dec(x_1);
|
||||
x_51 = lean_ctor_get(x_49, 0);
|
||||
lean_inc(x_51);
|
||||
x_52 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_51);
|
||||
x_52 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_51);
|
||||
lean_dec(x_51);
|
||||
x_53 = lean_ctor_get(x_49, 1);
|
||||
lean_inc(x_53);
|
||||
|
|
|
|||
6
stage0/stdlib/Lean/Parser/Term.c
generated
6
stage0/stdlib/Lean/Parser/Term.c
generated
|
|
@ -3094,7 +3094,6 @@ lean_object* l_Lean_Parser_Term_matchAlt_formatter___closed__2;
|
|||
lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__13;
|
||||
lean_object* l_Lean_Parser_Term_namedPattern___elambda__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_structInst_formatter___closed__20;
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_structInstField_parenthesizer___closed__4;
|
||||
lean_object* l_Lean_Parser_Term_whereDecls_formatter___closed__12;
|
||||
lean_object* l_Lean_Parser_Term_sort_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -3450,6 +3449,7 @@ lean_object* l_Lean_Parser_Term_ensureExpectedType___elambda__1___closed__6;
|
|||
lean_object* l_Lean_Parser_Term_let_x21___elambda__1___closed__2;
|
||||
lean_object* l_Lean_Parser_Tactic_quot___elambda__1___closed__11;
|
||||
lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__4;
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_bracketedBinder_formatter(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Term_matchDiscr___elambda__1___closed__15;
|
||||
lean_object* l_Lean_Parser_Term_let_x21_formatter___closed__2;
|
||||
|
|
@ -36684,7 +36684,7 @@ lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_35; uint8_
|
|||
x_8 = lean_ctor_get(x_6, 0);
|
||||
lean_inc(x_8);
|
||||
x_9 = lean_array_get_size(x_8);
|
||||
x_35 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_8);
|
||||
x_35 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_8);
|
||||
lean_dec(x_8);
|
||||
x_36 = l_Lean_Parser_Term_isIdent(x_35);
|
||||
lean_dec(x_35);
|
||||
|
|
@ -37181,7 +37181,7 @@ lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9;
|
|||
x_6 = lean_ctor_get(x_4, 0);
|
||||
lean_inc(x_6);
|
||||
x_7 = lean_array_get_size(x_6);
|
||||
x_8 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_6);
|
||||
x_8 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_6);
|
||||
lean_dec(x_6);
|
||||
x_9 = l_Lean_Parser_Term_isIdent(x_8);
|
||||
lean_dec(x_8);
|
||||
|
|
|
|||
1586
stage0/stdlib/Lean/Parser/Transform.c
generated
1586
stage0/stdlib/Lean/Parser/Transform.c
generated
File diff suppressed because it is too large
Load diff
15139
stage0/stdlib/Lean/ParserCompiler.c
generated
15139
stage0/stdlib/Lean/ParserCompiler.c
generated
File diff suppressed because it is too large
Load diff
|
|
@ -230,7 +230,6 @@ lean_object* lean_get_projection_info(lean_object*, lean_object*);
|
|||
lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_unresolveOpenDecls_match__1(lean_object*);
|
||||
extern lean_object* l_Lean_throwUnknownConstant___rarg___closed__2;
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabLit___closed__2;
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfScientific_match__1(lean_object*);
|
||||
lean_object* l_Array_anyMUnsafe_any___at_Lean_PrettyPrinter_Delaborator_delabLam___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppImplicit_match__1(lean_object*);
|
||||
|
|
@ -252,6 +251,7 @@ lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfScientific(lea
|
|||
lean_object* l_Array_anyMUnsafe_any___at_Lean_PrettyPrinter_Delaborator_hasIdent___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabMData_match__3(lean_object*);
|
||||
lean_object* l_Lean_Meta_forallTelescope___at___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabPatterns___spec__4(lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__3___closed__1;
|
||||
lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabDo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -307,7 +307,6 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabCoe___closed__2;
|
|||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabCoe___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppExplicit_match__1(lean_object*);
|
||||
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1127____closed__29;
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__4;
|
||||
extern lean_object* l_myMacro____x40_Init_Notation___hyg_9203____closed__17;
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabMData___closed__1;
|
||||
lean_object* l_Lean_getConstInfo___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -401,6 +400,7 @@ lean_object* l_Lean_getStructureFields(lean_object*, lean_object*);
|
|||
lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_shouldGroupWithNext___closed__2;
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__2___closed__3;
|
||||
lean_object* lean_array_to_list(lean_object*, lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__4;
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabLam___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Name_isAtomic(lean_object*);
|
||||
extern lean_object* l_Lean_PrettyPrinter_Delaborator_getExprKind___closed__4;
|
||||
|
|
@ -674,7 +674,6 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppImplicit_match__1___rarg(l
|
|||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabStructureInstance_match__2(lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppWithUnexpander___closed__1;
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_AppMatchState_discrs___default;
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabProj(lean_object*);
|
||||
lean_object* l_Array_mapIdxM_map___at___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabPatterns___spec__3___closed__2;
|
||||
extern lean_object* l_Lean_Parser_Term_inaccessible___elambda__1___closed__6;
|
||||
|
|
@ -717,6 +716,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabSort_match__2___rarg(lean_obj
|
|||
lean_object* l_ReaderT_pure___at_Lean_PrettyPrinter_Delaborator_instMonadQuotationDelabM___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetE_match__1(lean_object*);
|
||||
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabBinders___closed__1;
|
||||
uint8_t l_List_isEmpty___rarg(lean_object*);
|
||||
lean_object* lean_local_ctx_find(lean_object*, lean_object*);
|
||||
|
|
@ -738,6 +738,7 @@ lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppImplicit___lambda__3(lean_
|
|||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabDoElems___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch___lambda__3___closed__11;
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfScientific(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabProj(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch_match__1(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppWithUnexpander(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -746,7 +747,6 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabStr
|
|||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___closed__1;
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabForall___lambda__1___closed__1;
|
||||
lean_object* l___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_shouldGroupWithNext_match__1(lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
lean_object* l_Lean_Expr_isConstructorApp_x3f(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Delaborator_delabStructureInstance_match__1(lean_object*);
|
||||
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
|
||||
|
|
@ -13808,7 +13808,7 @@ if (x_29 == 0)
|
|||
lean_object* x_30; lean_object* x_31;
|
||||
lean_dec(x_26);
|
||||
lean_dec(x_14);
|
||||
x_30 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_1);
|
||||
x_30 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_1);
|
||||
lean_dec(x_1);
|
||||
x_31 = l_Lean_PrettyPrinter_Delaborator_delabLam___lambda__1(x_2, x_30, x_3, x_4, x_5, x_6, x_7, x_24);
|
||||
lean_dec(x_7);
|
||||
|
|
@ -13934,7 +13934,7 @@ case 3:
|
|||
lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95;
|
||||
lean_dec(x_26);
|
||||
lean_dec(x_18);
|
||||
x_81 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_1);
|
||||
x_81 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_1);
|
||||
lean_dec(x_1);
|
||||
x_82 = l_Array_empty___closed__1;
|
||||
x_83 = lean_array_push(x_82, x_81);
|
||||
|
|
@ -13944,10 +13944,10 @@ x_86 = l_Lean_nullKind___closed__2;
|
|||
x_87 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_87, 0, x_86);
|
||||
lean_ctor_set(x_87, 1, x_85);
|
||||
x_88 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_88 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_89 = lean_array_push(x_88, x_87);
|
||||
x_90 = lean_array_push(x_89, x_14);
|
||||
x_91 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_91 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_92 = lean_array_push(x_90, x_91);
|
||||
x_93 = l_Lean_Parser_Term_instBinder___elambda__1___closed__2;
|
||||
x_94 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -14171,7 +14171,7 @@ if (x_130 == 0)
|
|||
lean_object* x_131; lean_object* x_132;
|
||||
lean_dec(x_127);
|
||||
lean_dec(x_14);
|
||||
x_131 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_1);
|
||||
x_131 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_1);
|
||||
lean_dec(x_1);
|
||||
x_132 = l_Lean_PrettyPrinter_Delaborator_delabLam___lambda__1(x_2, x_131, x_3, x_4, x_5, x_6, x_7, x_125);
|
||||
lean_dec(x_7);
|
||||
|
|
@ -14297,7 +14297,7 @@ case 3:
|
|||
lean_object* x_182; lean_object* x_183; lean_object* x_184; lean_object* x_185; lean_object* x_186; lean_object* x_187; lean_object* x_188; lean_object* x_189; lean_object* x_190; lean_object* x_191; lean_object* x_192; lean_object* x_193; lean_object* x_194; lean_object* x_195; lean_object* x_196;
|
||||
lean_dec(x_127);
|
||||
lean_dec(x_18);
|
||||
x_182 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_1);
|
||||
x_182 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_1);
|
||||
lean_dec(x_1);
|
||||
x_183 = l_Array_empty___closed__1;
|
||||
x_184 = lean_array_push(x_183, x_182);
|
||||
|
|
@ -14307,10 +14307,10 @@ x_187 = l_Lean_nullKind___closed__2;
|
|||
x_188 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_188, 0, x_187);
|
||||
lean_ctor_set(x_188, 1, x_186);
|
||||
x_189 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_189 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_190 = lean_array_push(x_189, x_188);
|
||||
x_191 = lean_array_push(x_190, x_14);
|
||||
x_192 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_192 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_193 = lean_array_push(x_191, x_192);
|
||||
x_194 = l_Lean_Parser_Term_instBinder___elambda__1___closed__2;
|
||||
x_195 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -14961,7 +14961,7 @@ lean_dec(x_6);
|
|||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
x_88 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_1);
|
||||
x_88 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_1);
|
||||
x_89 = l_Array_empty___closed__1;
|
||||
x_90 = lean_array_push(x_89, x_88);
|
||||
x_91 = l_myMacro____x40_Init_Notation___hyg_11225____closed__10;
|
||||
|
|
@ -14970,10 +14970,10 @@ x_93 = l_Lean_nullKind___closed__2;
|
|||
x_94 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_94, 0, x_93);
|
||||
lean_ctor_set(x_94, 1, x_92);
|
||||
x_95 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_95 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_96 = lean_array_push(x_95, x_94);
|
||||
x_97 = lean_array_push(x_96, x_15);
|
||||
x_98 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_98 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_99 = lean_array_push(x_97, x_98);
|
||||
x_100 = l_Lean_Parser_Term_instBinder___elambda__1___closed__2;
|
||||
x_101 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -15301,7 +15301,7 @@ lean_dec(x_6);
|
|||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
x_195 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_1);
|
||||
x_195 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_1);
|
||||
x_196 = l_Array_empty___closed__1;
|
||||
x_197 = lean_array_push(x_196, x_195);
|
||||
x_198 = l_myMacro____x40_Init_Notation___hyg_11225____closed__10;
|
||||
|
|
@ -15310,10 +15310,10 @@ x_200 = l_Lean_nullKind___closed__2;
|
|||
x_201 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_201, 0, x_200);
|
||||
lean_ctor_set(x_201, 1, x_199);
|
||||
x_202 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_202 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_203 = lean_array_push(x_202, x_201);
|
||||
x_204 = lean_array_push(x_203, x_121);
|
||||
x_205 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_205 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_206 = lean_array_push(x_204, x_205);
|
||||
x_207 = l_Lean_Parser_Term_instBinder___elambda__1___closed__2;
|
||||
x_208 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -20393,7 +20393,7 @@ static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabNil___lambda__1_
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_1 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_2 = l_myMacro____x40_Init_Notation___hyg_9203____closed__20;
|
||||
x_3 = lean_array_push(x_1, x_2);
|
||||
return x_3;
|
||||
|
|
@ -20404,7 +20404,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_PrettyPrinter_Delaborator_delabNil___lambda__1___closed__1;
|
||||
x_2 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_2 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_3 = lean_array_push(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
@ -20682,9 +20682,9 @@ x_49 = lean_array_push(x_48, x_12);
|
|||
x_50 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_50, 0, x_40);
|
||||
lean_ctor_set(x_50, 1, x_49);
|
||||
x_51 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_51 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_52 = lean_array_push(x_51, x_50);
|
||||
x_53 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_53 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_54 = lean_array_push(x_52, x_53);
|
||||
x_55 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_55, 0, x_19);
|
||||
|
|
@ -20710,9 +20710,9 @@ x_31 = l_Lean_nullKind___closed__2;
|
|||
x_32 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_32, 0, x_31);
|
||||
lean_ctor_set(x_32, 1, x_30);
|
||||
x_33 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_33 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_34 = lean_array_push(x_33, x_32);
|
||||
x_35 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_35 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_36 = lean_array_push(x_34, x_35);
|
||||
x_37 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_37, 0, x_19);
|
||||
|
|
@ -20832,9 +20832,9 @@ x_97 = lean_array_push(x_96, x_60);
|
|||
x_98 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_98, 0, x_88);
|
||||
lean_ctor_set(x_98, 1, x_97);
|
||||
x_99 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_99 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_100 = lean_array_push(x_99, x_98);
|
||||
x_101 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_101 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_102 = lean_array_push(x_100, x_101);
|
||||
x_103 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_103, 0, x_67);
|
||||
|
|
@ -20861,9 +20861,9 @@ x_79 = l_Lean_nullKind___closed__2;
|
|||
x_80 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_80, 0, x_79);
|
||||
lean_ctor_set(x_80, 1, x_78);
|
||||
x_81 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__9;
|
||||
x_81 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__9;
|
||||
x_82 = lean_array_push(x_81, x_80);
|
||||
x_83 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_83 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_84 = lean_array_push(x_82, x_83);
|
||||
x_85 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_85, 0, x_67);
|
||||
|
|
@ -21110,7 +21110,7 @@ lean_ctor_set(x_23, 0, x_22);
|
|||
lean_ctor_set(x_23, 1, x_21);
|
||||
x_24 = l_Lean_PrettyPrinter_Delaborator_delabListToArray___lambda__1___closed__2;
|
||||
x_25 = lean_array_push(x_24, x_23);
|
||||
x_26 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_26 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_27 = lean_array_push(x_25, x_26);
|
||||
x_28 = l_term_x23_x5b___x2c_x5d___closed__2;
|
||||
x_29 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -21155,7 +21155,7 @@ lean_ctor_set(x_41, 0, x_40);
|
|||
lean_ctor_set(x_41, 1, x_39);
|
||||
x_42 = l_Lean_PrettyPrinter_Delaborator_delabListToArray___lambda__1___closed__2;
|
||||
x_43 = lean_array_push(x_42, x_41);
|
||||
x_44 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__10;
|
||||
x_44 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__10;
|
||||
x_45 = lean_array_push(x_43, x_44);
|
||||
x_46 = l_term_x23_x5b___x2c_x5d___closed__2;
|
||||
x_47 = lean_alloc_ctor(1, 2, 0);
|
||||
|
|
@ -21237,7 +21237,7 @@ _start:
|
|||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNil___closed__1;
|
||||
x_2 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__4;
|
||||
x_2 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__4;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
|
|
|
|||
10
stage0/stdlib/Lean/PrettyPrinter/Formatter.c
generated
10
stage0/stdlib/Lean/PrettyPrinter/Formatter.c
generated
|
|
@ -441,7 +441,6 @@ lean_object* l_Lean_PrettyPrinter_Formatter_instMonadTraverserFormatterM___close
|
|||
lean_object* l_Lean_PrettyPrinter_Formatter_identNoAntiquot_formatter_match__1(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Formatter_withoutInfo_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_array_pop(lean_object*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_idxsBack___spec__1(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Formatter_concat___lambda__1___boxed(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_throwError___at_Lean_Core_withIncRecDepth___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -490,6 +489,7 @@ lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_For
|
|||
lean_object* l_Lean_PrettyPrinter_Formatter_symbol_formatter___closed__11;
|
||||
extern lean_object* l_Lean_PrettyPrinter_backtrackExceptionId;
|
||||
lean_object* l_Lean_PrettyPrinter_Formatter_suppressInsideQuot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Formatter_initFn____x40_Lean_PrettyPrinter_Formatter___hyg_2502____closed__2;
|
||||
lean_object* l_Lean_Syntax_Traverser_left(lean_object*);
|
||||
lean_object* l_ReaderT_map___at_Lean_PrettyPrinter_Formatter_instMonadTraverserFormatterM___spec__1(lean_object*, lean_object*);
|
||||
|
|
@ -3797,12 +3797,12 @@ lean_inc(x_12);
|
|||
lean_dec(x_10);
|
||||
x_13 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_13);
|
||||
x_14 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_13);
|
||||
x_14 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_13);
|
||||
lean_dec(x_13);
|
||||
x_15 = lean_ctor_get(x_12, 2);
|
||||
lean_inc(x_15);
|
||||
lean_dec(x_12);
|
||||
x_16 = l_Array_back___at_Lean_Syntax_Traverser_idxsBack___spec__1(x_15);
|
||||
x_16 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_15);
|
||||
lean_dec(x_15);
|
||||
x_17 = lean_nat_sub(x_16, x_1);
|
||||
lean_dec(x_16);
|
||||
|
|
@ -3843,12 +3843,12 @@ lean_inc(x_13);
|
|||
lean_dec(x_11);
|
||||
x_14 = lean_ctor_get(x_13, 1);
|
||||
lean_inc(x_14);
|
||||
x_15 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_14);
|
||||
x_15 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_14);
|
||||
lean_dec(x_14);
|
||||
x_16 = lean_ctor_get(x_13, 2);
|
||||
lean_inc(x_16);
|
||||
lean_dec(x_13);
|
||||
x_17 = l_Array_back___at_Lean_Syntax_Traverser_idxsBack___spec__1(x_16);
|
||||
x_17 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_16);
|
||||
lean_dec(x_16);
|
||||
x_18 = lean_nat_sub(x_17, x_1);
|
||||
lean_dec(x_17);
|
||||
|
|
|
|||
78
stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c
generated
78
stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c
generated
|
|
@ -160,6 +160,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer(lean_objec
|
|||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_errorAtSavedPos_parenthesizer___rarg(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_parenthesizerForKind___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_back_x3f___rarg(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkPrec_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_unicodeSymbol_parenthesizer___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_sepByNoAntiquot_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -204,7 +205,6 @@ lean_object* l_Lean_Syntax_Traverser_setCur(lean_object*, lean_object*);
|
|||
extern lean_object* l_Lean_Parser_Tactic_intro___closed__12;
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_term_parenthesizer___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_term___x24_______closed__4;
|
||||
lean_object* l_Lean_Syntax_Traverser_idxsBack(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_addTrace___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_parenthesizerForKindUnsafe___closed__1;
|
||||
|
|
@ -482,7 +482,6 @@ lean_object* l_Lean_PrettyPrinter_mkCategoryParenthesizerAttribute___closed__2;
|
|||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_lookahead_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_IO_mkRef___at_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2401____spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___lambda__4___closed__1;
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_idxsBack___spec__1(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_mkCombinatorParenthesizerAttribute(lean_object*);
|
||||
lean_object* l_Lean_throwError___at_Lean_Core_withIncRecDepth___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
|
||||
|
|
@ -541,6 +540,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_instMonadQuotationParenthesizerM
|
|||
lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__6;
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkColGt_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_MonadTraverser_getIdx___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__1;
|
||||
lean_object* l_ReaderT_bind___at_Lean_PrettyPrinter_Parenthesizer_trailingNode_parenthesizer___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_initFn____x40_Lean_PrettyPrinter_Parenthesizer___hyg_2466____closed__14;
|
||||
|
|
@ -3340,33 +3340,69 @@ x_7 = lean_st_ref_get(x_1, x_6);
|
|||
x_8 = !lean_is_exclusive(x_7);
|
||||
if (x_8 == 0)
|
||||
{
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11;
|
||||
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
|
||||
x_9 = lean_ctor_get(x_7, 0);
|
||||
x_10 = lean_ctor_get(x_9, 0);
|
||||
lean_inc(x_10);
|
||||
lean_dec(x_9);
|
||||
x_11 = l_Lean_Syntax_Traverser_idxsBack(x_10);
|
||||
x_11 = lean_ctor_get(x_10, 2);
|
||||
lean_inc(x_11);
|
||||
lean_dec(x_10);
|
||||
lean_ctor_set(x_7, 0, x_11);
|
||||
x_12 = l_Array_back_x3f___rarg(x_11);
|
||||
lean_dec(x_11);
|
||||
if (lean_obj_tag(x_12) == 0)
|
||||
{
|
||||
lean_object* x_13;
|
||||
x_13 = lean_unsigned_to_nat(0u);
|
||||
lean_ctor_set(x_7, 0, x_13);
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
|
||||
x_12 = lean_ctor_get(x_7, 0);
|
||||
x_13 = lean_ctor_get(x_7, 1);
|
||||
lean_inc(x_13);
|
||||
lean_inc(x_12);
|
||||
lean_dec(x_7);
|
||||
lean_object* x_14;
|
||||
x_14 = lean_ctor_get(x_12, 0);
|
||||
lean_inc(x_14);
|
||||
lean_dec(x_12);
|
||||
x_15 = l_Lean_Syntax_Traverser_idxsBack(x_14);
|
||||
lean_dec(x_14);
|
||||
x_16 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_16, 0, x_15);
|
||||
lean_ctor_set(x_16, 1, x_13);
|
||||
return x_16;
|
||||
lean_ctor_set(x_7, 0, x_14);
|
||||
return x_7;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
|
||||
x_15 = lean_ctor_get(x_7, 0);
|
||||
x_16 = lean_ctor_get(x_7, 1);
|
||||
lean_inc(x_16);
|
||||
lean_inc(x_15);
|
||||
lean_dec(x_7);
|
||||
x_17 = lean_ctor_get(x_15, 0);
|
||||
lean_inc(x_17);
|
||||
lean_dec(x_15);
|
||||
x_18 = lean_ctor_get(x_17, 2);
|
||||
lean_inc(x_18);
|
||||
lean_dec(x_17);
|
||||
x_19 = l_Array_back_x3f___rarg(x_18);
|
||||
lean_dec(x_18);
|
||||
if (lean_obj_tag(x_19) == 0)
|
||||
{
|
||||
lean_object* x_20; lean_object* x_21;
|
||||
x_20 = lean_unsigned_to_nat(0u);
|
||||
x_21 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_21, 0, x_20);
|
||||
lean_ctor_set(x_21, 1, x_16);
|
||||
return x_21;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_22; lean_object* x_23;
|
||||
x_22 = lean_ctor_get(x_19, 0);
|
||||
lean_inc(x_22);
|
||||
lean_dec(x_19);
|
||||
x_23 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_23, 0, x_22);
|
||||
lean_ctor_set(x_23, 1, x_16);
|
||||
return x_23;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -7342,12 +7378,12 @@ lean_inc(x_13);
|
|||
lean_dec(x_11);
|
||||
x_14 = lean_ctor_get(x_13, 1);
|
||||
lean_inc(x_14);
|
||||
x_15 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_14);
|
||||
x_15 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_14);
|
||||
lean_dec(x_14);
|
||||
x_16 = lean_ctor_get(x_13, 2);
|
||||
lean_inc(x_16);
|
||||
lean_dec(x_13);
|
||||
x_17 = l_Array_back___at_Lean_Syntax_Traverser_idxsBack___spec__1(x_16);
|
||||
x_17 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_16);
|
||||
lean_dec(x_16);
|
||||
x_18 = lean_nat_sub(x_17, x_1);
|
||||
lean_dec(x_17);
|
||||
|
|
@ -7388,12 +7424,12 @@ lean_inc(x_13);
|
|||
lean_dec(x_11);
|
||||
x_14 = lean_ctor_get(x_13, 1);
|
||||
lean_inc(x_14);
|
||||
x_15 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_14);
|
||||
x_15 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_14);
|
||||
lean_dec(x_14);
|
||||
x_16 = lean_ctor_get(x_13, 2);
|
||||
lean_inc(x_16);
|
||||
lean_dec(x_13);
|
||||
x_17 = l_Array_back___at_Lean_Syntax_Traverser_idxsBack___spec__1(x_16);
|
||||
x_17 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_16);
|
||||
lean_dec(x_16);
|
||||
x_18 = lean_nat_sub(x_17, x_1);
|
||||
lean_dec(x_17);
|
||||
|
|
|
|||
330
stage0/stdlib/Lean/Server/ServerBin.c
generated
330
stage0/stdlib/Lean/Server/ServerBin.c
generated
|
|
@ -1,330 +0,0 @@
|
|||
// Lean compiler output
|
||||
// Module: Lean.Server.ServerBin
|
||||
// Imports: Init Init.System.IO Lean.Server
|
||||
#include <lean/lean.h>
|
||||
#if defined(__clang__)
|
||||
#pragma clang diagnostic ignored "-Wunused-parameter"
|
||||
#pragma clang diagnostic ignored "-Wunused-label"
|
||||
#elif defined(__GNUC__) && !defined(__CLANG__)
|
||||
#pragma GCC diagnostic ignored "-Wunused-parameter"
|
||||
#pragma GCC diagnostic ignored "-Wunused-label"
|
||||
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
|
||||
#endif
|
||||
#ifdef __cplusplus
|
||||
extern "C" {
|
||||
#endif
|
||||
lean_object* lean_get_stdin(lean_object*);
|
||||
lean_object* lean_io_error_to_string(lean_object*);
|
||||
lean_object* _lean_main(lean_object*, lean_object*);
|
||||
lean_object* lean_get_stderr(lean_object*);
|
||||
lean_object* l_main___boxed__const__1;
|
||||
lean_object* l_IO_getStdin___at_main___spec__1(lean_object*);
|
||||
lean_object* lean_init_search_path(lean_object*, lean_object*);
|
||||
lean_object* lean_get_stdout(lean_object*);
|
||||
lean_object* l_IO_FS_Stream_putStrLn___at_Lean_Server_Test_runWithInputFile___spec__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Server_initAndRunServer(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_IO_getStdin___at_main___spec__1(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_get_stdin(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_main___boxed__const__1() {
|
||||
_start:
|
||||
{
|
||||
uint32_t x_1; lean_object* x_2;
|
||||
x_1 = 0;
|
||||
x_2 = lean_box_uint32(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* _lean_main(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
lean_dec(x_1);
|
||||
x_3 = lean_get_stdin(x_2);
|
||||
if (lean_obj_tag(x_3) == 0)
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
||||
x_4 = lean_ctor_get(x_3, 0);
|
||||
lean_inc(x_4);
|
||||
x_5 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_5);
|
||||
lean_dec(x_3);
|
||||
x_6 = lean_get_stdout(x_5);
|
||||
if (lean_obj_tag(x_6) == 0)
|
||||
{
|
||||
lean_object* x_7; lean_object* x_8; lean_object* x_9;
|
||||
x_7 = lean_ctor_get(x_6, 0);
|
||||
lean_inc(x_7);
|
||||
x_8 = lean_ctor_get(x_6, 1);
|
||||
lean_inc(x_8);
|
||||
lean_dec(x_6);
|
||||
x_9 = lean_get_stderr(x_8);
|
||||
if (lean_obj_tag(x_9) == 0)
|
||||
{
|
||||
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
|
||||
x_10 = lean_ctor_get(x_9, 0);
|
||||
lean_inc(x_10);
|
||||
x_11 = lean_ctor_get(x_9, 1);
|
||||
lean_inc(x_11);
|
||||
lean_dec(x_9);
|
||||
x_12 = lean_box(0);
|
||||
x_13 = lean_init_search_path(x_12, x_11);
|
||||
if (lean_obj_tag(x_13) == 0)
|
||||
{
|
||||
lean_object* x_14; lean_object* x_15;
|
||||
x_14 = lean_ctor_get(x_13, 1);
|
||||
lean_inc(x_14);
|
||||
lean_dec(x_13);
|
||||
x_15 = l_Lean_Server_initAndRunServer(x_4, x_7, x_14);
|
||||
if (lean_obj_tag(x_15) == 0)
|
||||
{
|
||||
uint8_t x_16;
|
||||
lean_dec(x_10);
|
||||
x_16 = !lean_is_exclusive(x_15);
|
||||
if (x_16 == 0)
|
||||
{
|
||||
lean_object* x_17; lean_object* x_18;
|
||||
x_17 = lean_ctor_get(x_15, 0);
|
||||
lean_dec(x_17);
|
||||
x_18 = l_main___boxed__const__1;
|
||||
lean_ctor_set(x_15, 0, x_18);
|
||||
return x_15;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_19; lean_object* x_20; lean_object* x_21;
|
||||
x_19 = lean_ctor_get(x_15, 1);
|
||||
lean_inc(x_19);
|
||||
lean_dec(x_15);
|
||||
x_20 = l_main___boxed__const__1;
|
||||
x_21 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_21, 0, x_20);
|
||||
lean_ctor_set(x_21, 1, x_19);
|
||||
return x_21;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
|
||||
x_22 = lean_ctor_get(x_15, 0);
|
||||
lean_inc(x_22);
|
||||
x_23 = lean_ctor_get(x_15, 1);
|
||||
lean_inc(x_23);
|
||||
lean_dec(x_15);
|
||||
x_24 = lean_io_error_to_string(x_22);
|
||||
x_25 = l_IO_FS_Stream_putStrLn___at_Lean_Server_Test_runWithInputFile___spec__1(x_10, x_24, x_23);
|
||||
if (lean_obj_tag(x_25) == 0)
|
||||
{
|
||||
uint8_t x_26;
|
||||
x_26 = !lean_is_exclusive(x_25);
|
||||
if (x_26 == 0)
|
||||
{
|
||||
lean_object* x_27; lean_object* x_28;
|
||||
x_27 = lean_ctor_get(x_25, 0);
|
||||
lean_dec(x_27);
|
||||
x_28 = l_main___boxed__const__1;
|
||||
lean_ctor_set(x_25, 0, x_28);
|
||||
return x_25;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_29; lean_object* x_30; lean_object* x_31;
|
||||
x_29 = lean_ctor_get(x_25, 1);
|
||||
lean_inc(x_29);
|
||||
lean_dec(x_25);
|
||||
x_30 = l_main___boxed__const__1;
|
||||
x_31 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_31, 0, x_30);
|
||||
lean_ctor_set(x_31, 1, x_29);
|
||||
return x_31;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_32;
|
||||
x_32 = !lean_is_exclusive(x_25);
|
||||
if (x_32 == 0)
|
||||
{
|
||||
return x_25;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_33; lean_object* x_34; lean_object* x_35;
|
||||
x_33 = lean_ctor_get(x_25, 0);
|
||||
x_34 = lean_ctor_get(x_25, 1);
|
||||
lean_inc(x_34);
|
||||
lean_inc(x_33);
|
||||
lean_dec(x_25);
|
||||
x_35 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_35, 0, x_33);
|
||||
lean_ctor_set(x_35, 1, x_34);
|
||||
return x_35;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_36;
|
||||
lean_dec(x_10);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_4);
|
||||
x_36 = !lean_is_exclusive(x_13);
|
||||
if (x_36 == 0)
|
||||
{
|
||||
return x_13;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_37; lean_object* x_38; lean_object* x_39;
|
||||
x_37 = lean_ctor_get(x_13, 0);
|
||||
x_38 = lean_ctor_get(x_13, 1);
|
||||
lean_inc(x_38);
|
||||
lean_inc(x_37);
|
||||
lean_dec(x_13);
|
||||
x_39 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_39, 0, x_37);
|
||||
lean_ctor_set(x_39, 1, x_38);
|
||||
return x_39;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_40;
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_4);
|
||||
x_40 = !lean_is_exclusive(x_9);
|
||||
if (x_40 == 0)
|
||||
{
|
||||
return x_9;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_41; lean_object* x_42; lean_object* x_43;
|
||||
x_41 = lean_ctor_get(x_9, 0);
|
||||
x_42 = lean_ctor_get(x_9, 1);
|
||||
lean_inc(x_42);
|
||||
lean_inc(x_41);
|
||||
lean_dec(x_9);
|
||||
x_43 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_43, 0, x_41);
|
||||
lean_ctor_set(x_43, 1, x_42);
|
||||
return x_43;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_44;
|
||||
lean_dec(x_4);
|
||||
x_44 = !lean_is_exclusive(x_6);
|
||||
if (x_44 == 0)
|
||||
{
|
||||
return x_6;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_45; lean_object* x_46; lean_object* x_47;
|
||||
x_45 = lean_ctor_get(x_6, 0);
|
||||
x_46 = lean_ctor_get(x_6, 1);
|
||||
lean_inc(x_46);
|
||||
lean_inc(x_45);
|
||||
lean_dec(x_6);
|
||||
x_47 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_47, 0, x_45);
|
||||
lean_ctor_set(x_47, 1, x_46);
|
||||
return x_47;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_48;
|
||||
x_48 = !lean_is_exclusive(x_3);
|
||||
if (x_48 == 0)
|
||||
{
|
||||
return x_3;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_49; lean_object* x_50; lean_object* x_51;
|
||||
x_49 = lean_ctor_get(x_3, 0);
|
||||
x_50 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_50);
|
||||
lean_inc(x_49);
|
||||
lean_dec(x_3);
|
||||
x_51 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_51, 0, x_49);
|
||||
lean_ctor_set(x_51, 1, x_50);
|
||||
return x_51;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* initialize_Init(lean_object*);
|
||||
lean_object* initialize_Init_System_IO(lean_object*);
|
||||
lean_object* initialize_Lean_Server(lean_object*);
|
||||
static bool _G_initialized = false;
|
||||
lean_object* initialize_Lean_Server_ServerBin(lean_object* w) {
|
||||
lean_object * res;
|
||||
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
|
||||
_G_initialized = true;
|
||||
res = initialize_Init(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Init_System_IO(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
res = initialize_Lean_Server(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_main___boxed__const__1 = _init_l_main___boxed__const__1();
|
||||
lean_mark_persistent(l_main___boxed__const__1);
|
||||
return lean_io_result_mk_ok(lean_box(0));
|
||||
}
|
||||
void lean_initialize();
|
||||
|
||||
#if defined(WIN32) || defined(_WIN32)
|
||||
#include <windows.h>
|
||||
#endif
|
||||
|
||||
int main(int argc, char ** argv) {
|
||||
#if defined(WIN32) || defined(_WIN32)
|
||||
SetErrorMode(SEM_FAILCRITICALERRORS);
|
||||
#endif
|
||||
lean_object* in; lean_object* res;
|
||||
lean_initialize();
|
||||
res = initialize_Lean_Server_ServerBin(lean_io_mk_world());
|
||||
lean_io_mark_end_initialization();
|
||||
if (lean_io_result_is_ok(res)) {
|
||||
lean_dec_ref(res);
|
||||
lean_init_task_manager();
|
||||
in = lean_box(0);
|
||||
int i = argc;
|
||||
while (i > 1) {
|
||||
lean_object* n;
|
||||
i--;
|
||||
n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);
|
||||
in = n;
|
||||
}
|
||||
res = _lean_main(in, lean_io_mk_world());
|
||||
}
|
||||
if (lean_io_result_is_ok(res)) {
|
||||
int ret = lean_unbox(lean_io_result_get_value(res));
|
||||
lean_dec_ref(res);
|
||||
return ret;
|
||||
} else {
|
||||
lean_io_result_show_error(res);
|
||||
lean_dec_ref(res);
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
#ifdef __cplusplus
|
||||
}
|
||||
#endif
|
||||
167
stage0/stdlib/Lean/Syntax.c
generated
167
stage0/stdlib/Lean/Syntax.c
generated
|
|
@ -106,6 +106,7 @@ lean_object* l_Lean_Syntax_getAntiquotTerm___boxed(lean_object*);
|
|||
uint8_t l_USize_decLt(size_t, size_t);
|
||||
extern lean_object* l_term___x24_______closed__5;
|
||||
lean_object* l_Lean_Syntax_MonadTraverser_goDown(lean_object*);
|
||||
lean_object* l_Array_back_x3f___rarg(lean_object*);
|
||||
lean_object* l_Lean_Syntax_mkAntiquotNode(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
|
||||
lean_object* l_Lean_Syntax_modifyArgs_match__1(lean_object*);
|
||||
lean_object* l_List_map___at_Lean_Syntax_formatStxAux___spec__4(lean_object*, uint8_t, lean_object*, lean_object*);
|
||||
|
|
@ -136,7 +137,6 @@ lean_object* l_Lean_SyntaxNode_getIdAt(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Syntax_antiquotKind_x3f___boxed(lean_object*);
|
||||
lean_object* l_Lean_Syntax_MonadTraverser_getIdx___rarg___lambda__1___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_replaceM___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_Traverser_idxsBack(lean_object*);
|
||||
lean_object* lean_array_fget(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_getKind___boxed(lean_object*);
|
||||
lean_object* l_Lean_Syntax_instBEqSyntax;
|
||||
|
|
@ -231,6 +231,7 @@ uint8_t l_Lean_Syntax_isAntiquot(lean_object*);
|
|||
lean_object* l_Lean_Syntax_ifNode___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_mkAntiquotNode___closed__17;
|
||||
lean_object* l_Lean_Syntax_instToStringSyntax;
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2___boxed(lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_getNumArgs___boxed(lean_object*);
|
||||
lean_object* l_Lean_Format_joinSep___at_Lean_Syntax_formatStxAux___spec__2___boxed(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Format_sbracket___closed__3;
|
||||
|
|
@ -276,7 +277,6 @@ lean_object* l_Lean_Syntax_Traverser_right(lean_object*);
|
|||
lean_object* l_Lean_SyntaxNode_withArgs___rarg(lean_object*, lean_object*);
|
||||
lean_object* lean_panic_fn(lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Syntax_isAntiquotSplicePat(lean_object*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_idxsBack___spec__1___boxed(lean_object*);
|
||||
lean_object* l_Lean_Syntax_instToStringSyntax___closed__2;
|
||||
lean_object* l_Lean_SyntaxNode_modifyArgs_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Format_paren___closed__2;
|
||||
|
|
@ -307,7 +307,6 @@ extern lean_object* l_myMacro____x40_Init_Notation___hyg_9203____closed__21;
|
|||
lean_object* lean_array_pop(lean_object*);
|
||||
lean_object* l_Lean_Syntax_ifNode_match__1(lean_object*);
|
||||
lean_object* lean_mk_array(lean_object*, lean_object*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_idxsBack___spec__1(lean_object*);
|
||||
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Syntax_0__Lean_Syntax_updateLeadingAux(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkListNode(lean_object*);
|
||||
|
|
@ -334,6 +333,7 @@ extern lean_object* l_stx___x2a___closed__3;
|
|||
lean_object* l_Lean_Syntax_getAtomVal_x21(lean_object*);
|
||||
lean_object* l_List_map___at_Lean_Syntax_formatStxAux___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_ifNodeKind___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_getKind_match__1(lean_object*);
|
||||
lean_object* l_Lean_Syntax_Traverser_left(lean_object*);
|
||||
lean_object* l_Lean_Syntax_mkAntiquotNode_match__3(lean_object*);
|
||||
|
|
@ -341,7 +341,6 @@ lean_object* l_Lean_Syntax_isQuot___boxed(lean_object*);
|
|||
lean_object* l_Lean_Syntax_modifyArgs(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_structEq_match__1(lean_object*);
|
||||
lean_object* l_Lean_Name_replacePrefix(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_Traverser_idxsBack___boxed(lean_object*);
|
||||
lean_object* l_Lean_SyntaxNode_getArg(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_antiquotKind_x3f(lean_object*);
|
||||
lean_object* l_Array_mapMUnsafe_map___at_Lean_Syntax_rewriteBottomUp___spec__2(lean_object*, size_t, size_t, lean_object*);
|
||||
|
|
@ -5778,58 +5777,6 @@ x_1 = l_Lean_Syntax_instBEqSyntax___closed__1;
|
|||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_idxsBack___spec__1(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
||||
x_2 = lean_array_get_size(x_1);
|
||||
x_3 = lean_unsigned_to_nat(1u);
|
||||
x_4 = lean_nat_sub(x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
x_5 = l_instInhabitedNat;
|
||||
x_6 = lean_array_get(x_5, x_1, x_4);
|
||||
lean_dec(x_4);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_Traverser_idxsBack(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; uint8_t x_3;
|
||||
x_2 = lean_ctor_get(x_1, 2);
|
||||
x_3 = l_Array_isEmpty___rarg(x_2);
|
||||
if (x_3 == 0)
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_Array_back___at_Lean_Syntax_Traverser_idxsBack___spec__1(x_2);
|
||||
return x_4;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_5;
|
||||
x_5 = lean_unsigned_to_nat(0u);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_idxsBack___spec__1___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_Array_back___at_Lean_Syntax_Traverser_idxsBack___spec__1(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_Traverser_idxsBack___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_Lean_Syntax_Traverser_idxsBack(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_Traverser_fromSyntax(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -5926,6 +5873,20 @@ x_2 = lean_array_get_size(x_1);
|
|||
x_3 = lean_unsigned_to_nat(1u);
|
||||
x_4 = lean_nat_sub(x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
x_5 = l_instInhabitedNat;
|
||||
x_6 = lean_array_get(x_5, x_1, x_4);
|
||||
lean_dec(x_4);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
|
||||
x_2 = lean_array_get_size(x_1);
|
||||
x_3 = lean_unsigned_to_nat(1u);
|
||||
x_4 = lean_nat_sub(x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
x_5 = l_Lean_instInhabitedSyntax;
|
||||
x_6 = lean_array_get(x_5, x_1, x_4);
|
||||
lean_dec(x_4);
|
||||
|
|
@ -5949,24 +5910,24 @@ return x_1;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
|
||||
x_6 = l_Lean_Syntax_Traverser_idxsBack(x_1);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_2);
|
||||
x_8 = l_Lean_Syntax_getNumArgs(x_7);
|
||||
x_9 = lean_nat_dec_lt(x_6, x_8);
|
||||
lean_dec(x_8);
|
||||
x_10 = lean_array_pop(x_2);
|
||||
x_11 = lean_ctor_get(x_1, 2);
|
||||
lean_inc(x_11);
|
||||
x_12 = lean_array_pop(x_11);
|
||||
if (x_9 == 0)
|
||||
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; lean_object* x_12;
|
||||
x_6 = lean_ctor_get(x_1, 2);
|
||||
lean_inc(x_6);
|
||||
x_7 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_6);
|
||||
x_8 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_2);
|
||||
x_9 = l_Lean_Syntax_getNumArgs(x_8);
|
||||
x_10 = lean_nat_dec_lt(x_7, x_9);
|
||||
lean_dec(x_9);
|
||||
x_11 = lean_array_pop(x_2);
|
||||
x_12 = lean_array_pop(x_6);
|
||||
if (x_10 == 0)
|
||||
{
|
||||
lean_object* x_13;
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_1);
|
||||
x_13 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_13, 0, x_7);
|
||||
lean_ctor_set(x_13, 1, x_10);
|
||||
lean_ctor_set(x_13, 0, x_8);
|
||||
lean_ctor_set(x_13, 1, x_11);
|
||||
lean_ctor_set(x_13, 2, x_12);
|
||||
return x_13;
|
||||
}
|
||||
|
|
@ -5976,11 +5937,11 @@ lean_object* x_14; lean_object* x_15; lean_object* x_16;
|
|||
x_14 = lean_ctor_get(x_1, 0);
|
||||
lean_inc(x_14);
|
||||
lean_dec(x_1);
|
||||
x_15 = l_Lean_Syntax_setArg(x_7, x_6, x_14);
|
||||
lean_dec(x_6);
|
||||
x_15 = l_Lean_Syntax_setArg(x_8, x_7, x_14);
|
||||
lean_dec(x_7);
|
||||
x_16 = lean_alloc_ctor(0, 3, 0);
|
||||
lean_ctor_set(x_16, 0, x_15);
|
||||
lean_ctor_set(x_16, 1, x_10);
|
||||
lean_ctor_set(x_16, 1, x_11);
|
||||
lean_ctor_set(x_16, 2, x_12);
|
||||
return x_16;
|
||||
}
|
||||
|
|
@ -5996,6 +5957,15 @@ lean_dec(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_Traverser_left(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -6013,16 +5983,19 @@ return x_1;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
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_inc(x_1);
|
||||
x_6 = l_Lean_Syntax_Traverser_up(x_1);
|
||||
x_7 = l_Lean_Syntax_Traverser_idxsBack(x_1);
|
||||
x_7 = lean_ctor_get(x_1, 2);
|
||||
lean_inc(x_7);
|
||||
lean_dec(x_1);
|
||||
x_8 = lean_unsigned_to_nat(1u);
|
||||
x_9 = lean_nat_sub(x_7, x_8);
|
||||
x_8 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_7);
|
||||
lean_dec(x_7);
|
||||
x_10 = l_Lean_Syntax_Traverser_down(x_6, x_9);
|
||||
return x_10;
|
||||
x_9 = lean_unsigned_to_nat(1u);
|
||||
x_10 = lean_nat_sub(x_8, x_9);
|
||||
lean_dec(x_8);
|
||||
x_11 = l_Lean_Syntax_Traverser_down(x_6, x_10);
|
||||
return x_11;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -6043,16 +6016,19 @@ return x_1;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
|
||||
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_inc(x_1);
|
||||
x_6 = l_Lean_Syntax_Traverser_up(x_1);
|
||||
x_7 = l_Lean_Syntax_Traverser_idxsBack(x_1);
|
||||
x_7 = lean_ctor_get(x_1, 2);
|
||||
lean_inc(x_7);
|
||||
lean_dec(x_1);
|
||||
x_8 = lean_unsigned_to_nat(1u);
|
||||
x_9 = lean_nat_add(x_7, x_8);
|
||||
x_8 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__1(x_7);
|
||||
lean_dec(x_7);
|
||||
x_10 = l_Lean_Syntax_Traverser_down(x_6, x_9);
|
||||
return x_10;
|
||||
x_9 = lean_unsigned_to_nat(1u);
|
||||
x_10 = lean_nat_add(x_8, x_9);
|
||||
lean_dec(x_8);
|
||||
x_11 = l_Lean_Syntax_Traverser_down(x_6, x_10);
|
||||
return x_11;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -6307,9 +6283,24 @@ lean_dec(x_1);
|
|||
x_4 = lean_ctor_get(x_3, 1);
|
||||
lean_inc(x_4);
|
||||
lean_dec(x_3);
|
||||
x_5 = l_Lean_Syntax_Traverser_idxsBack(x_2);
|
||||
x_6 = lean_apply_2(x_4, lean_box(0), x_5);
|
||||
return x_6;
|
||||
x_5 = lean_ctor_get(x_2, 2);
|
||||
x_6 = l_Array_back_x3f___rarg(x_5);
|
||||
if (lean_obj_tag(x_6) == 0)
|
||||
{
|
||||
lean_object* x_7; lean_object* x_8;
|
||||
x_7 = lean_unsigned_to_nat(0u);
|
||||
x_8 = lean_apply_2(x_4, lean_box(0), x_7);
|
||||
return x_8;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_9; lean_object* x_10;
|
||||
x_9 = lean_ctor_get(x_6, 0);
|
||||
lean_inc(x_9);
|
||||
lean_dec(x_6);
|
||||
x_10 = lean_apply_2(x_4, lean_box(0), x_9);
|
||||
return x_10;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Syntax_MonadTraverser_getIdx___rarg(lean_object* x_1, lean_object* x_2) {
|
||||
|
|
|
|||
4
stage0/stdlib/Lean/ToExpr.c
generated
4
stage0/stdlib/Lean/ToExpr.c
generated
|
|
@ -80,12 +80,12 @@ lean_object* l_Lean_instToExprList___rarg___closed__1;
|
|||
lean_object* l_Lean_instToExprNat;
|
||||
lean_object* l_Lean_instToExprBool___lambda__1___closed__2;
|
||||
lean_object* l_Lean_List_toExprAux_match__1(lean_object*, lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
lean_object* l_Lean_instToExprName___closed__3;
|
||||
lean_object* l_Lean_List_toExprAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_instToExprUnit___lambda__1(lean_object*);
|
||||
lean_object* l_Lean_instToExprProd___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_instQuoteBool___closed__2;
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_instToExprUnit___closed__2;
|
||||
lean_object* l_Lean_List_toExprAux_match__1___rarg(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -910,7 +910,7 @@ static lean_object* _init_l_Lean_instToExprArray___rarg___lambda__1___closed__1(
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
x_1 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
x_2 = l_Lean_instToExprOption___rarg___lambda__1___closed__1;
|
||||
x_3 = l_Lean_mkConst(x_1, x_2);
|
||||
return x_3;
|
||||
|
|
|
|||
4
stage0/stdlib/Lean/Util/Recognizers.c
generated
4
stage0/stdlib/Lean/Util/Recognizers.c
generated
|
|
@ -59,9 +59,9 @@ lean_object* l_Lean_Expr_app3_x3f(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Expr_heq_x3f___boxed(lean_object*);
|
||||
lean_object* l_Lean_Expr_app1_x3f___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Expr_app2_x3f___boxed(lean_object*, lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Expr_arrow_x3f(lean_object*);
|
||||
extern lean_object* l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
lean_object* l_Lean_Expr_isConstructorApp_x3f_match__3(lean_object*);
|
||||
lean_object* l_Lean_Expr_constructorApp_x3f_match__1(lean_object*);
|
||||
lean_object* l_Lean_Expr_isConstructorApp_x3f___closed__1;
|
||||
|
|
@ -610,7 +610,7 @@ lean_object* l_Lean_Expr_arrayLit_x3f(lean_object* x_1) {
|
|||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; uint8_t x_4;
|
||||
x_2 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3393____closed__5;
|
||||
x_2 = l_myMacro____x40_Init_Data_Array_Basic___hyg_3405____closed__5;
|
||||
x_3 = lean_unsigned_to_nat(2u);
|
||||
x_4 = l_Lean_Expr_isAppOfArity(x_1, x_2, x_3);
|
||||
if (x_4 == 0)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue