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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-14 08:09:55 -08:00
parent 54e5ca0c7b
commit 38d2cffa7e
22 changed files with 14130 additions and 8881 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
stage0/src/Init/Lean/Meta/Basic.lean
View file

@ -59,10 +59,14 @@ end TransparencyMode
structure Config :=
(opts : Options := {})
-- TODO: merge all *Approx flags.
(foApprox : Bool := false)
(ctxApprox : Bool := false)
(quasiPatternApprox : Bool := false)
/- When `constApprox` is set to true,
we solve `?m t =?= c` using
`?m := fun _ => c`
when `?m t` is not a higher-order pattern and `c` is not an application as -/
(constApprox : Bool := false)
/-
When the following flag is set,
`isDefEq` throws the exeption `Exeption.isDefEqStuck`
@ -255,18 +259,19 @@ ctx ← read; pure ctx.config.opts
@[inline] def isReducible (constName : Name) : MetaM Bool := do
env ← getEnv; pure $ isReducible env constName
/-- While executing `x`, ensure the given transparency mode is used. -/
@[inline] def usingTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
adaptReader
(fun (ctx : Context) => { config := { transparency := mode, .. ctx.config }, .. ctx })
x
@[inline] def withConfig {α} (f : Config → Config) (x : MetaM α) : MetaM α :=
adaptReader (fun (ctx : Context) => { config := f ctx.config, .. ctx }) x
@[inline] def usingAtLeastTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
adaptReader
(fun (ctx : Context) =>
let oldMode := ctx.config.transparency;
/-- While executing `x`, ensure the given transparency mode is used. -/
@[inline] def withTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
withConfig (fun config => { transparency := mode, .. config }) x
@[inline] def withAtLeastTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
withConfig
(fun config =>
let oldMode := config.transparency;
let mode := if oldMode.lt mode then mode else oldMode;
{ config := { transparency := mode, .. ctx.config }, .. ctx })
{ transparency := mode, .. config })
x
def isSyntheticExprMVar (mvarId : MVarId) : MetaM Bool := do
@ -553,7 +558,7 @@ else
k #[] type
partial def isClassExpensive : Expr → MetaM (Option Name)
| type => usingTransparency TransparencyMode.reducible $ -- when testing whether a type is a type class, we only unfold reducible constants.
| type => withTransparency TransparencyMode.reducible $ -- when testing whether a type is a type class, we only unfold reducible constants.
forallTelescopeReducingAux isClassExpensive type none $ fun xs type => do
match type.getAppFn with
| Expr.const c _ _ => do
@ -700,14 +705,12 @@ mvarId ← mkFreshId;
modify $ fun s => { mctx := s.mctx.addLevelMVarDecl mvarId, .. s };
pure mvarId
def whnfUsingDefault : Expr → MetaM Expr :=
fun e => usingTransparency TransparencyMode.default $ whnf e
abbrev whnfD := whnfUsingDefault
def whnfD : Expr → MetaM Expr :=
fun e => withTransparency TransparencyMode.default $ whnf e
/-- Execute `x` using approximate unification. -/
@[inline] def approxDefEq {α} (x : MetaM α) : MetaM α :=
adaptReader (fun (ctx : Context) => { config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true, .. ctx.config }, .. ctx })
adaptReader (fun (ctx : Context) => { config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true, constApprox := true, .. ctx.config }, .. ctx })
x
@[inline] private def withNewFVar {α} (fvar fvarType : Expr) (k : Expr → MetaM α) : MetaM α := do

2
stage0/src/Init/Lean/Meta/Check.lean
View file

@ -79,7 +79,7 @@ private partial def checkAux : Expr → MetaM Unit
def check (e : Expr) : MetaM Unit :=
traceCtx `Meta.check $
usingTransparency TransparencyMode.all $ checkAux e
withTransparency TransparencyMode.all $ checkAux e
def isTypeCorrect (e : Expr) : MetaM Bool :=
catch

6
stage0/src/Init/Lean/Meta/DiscrTree.lean
View file

@ -182,7 +182,7 @@ partial def mkPathAux : Array Expr → Array Key → MetaM (Array Key)
private def initCapacity := 8
def mkPath (e : Expr) : MetaM (Array Key) :=
usingTransparency TransparencyMode.reducible $ do
withTransparency TransparencyMode.reducible $ do
let todo : Array Expr := Array.mkEmpty initCapacity;
let keys : Array Key := Array.mkEmpty initCapacity;
mkPathAux (todo.push e) keys
@ -309,7 +309,7 @@ match d.root.find Key.star with
| some (Trie.node vs _) => result ++ vs
def getMatch {α} (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
usingTransparency TransparencyMode.reducible $ do
withTransparency TransparencyMode.reducible $ do
let result := getStarResult d;
(k, args) ← getMatchKeyArgs e;
match k with
@ -341,7 +341,7 @@ private partial def getUnifyAux {α} : Nat → Array Expr → Trie α → (Array
| some c => do result ← visitStarChild result; getUnifyAux 0 (todo ++ args) c.2 result
def getUnify {α} (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
usingTransparency TransparencyMode.reducible $ do
withTransparency TransparencyMode.reducible $ do
(k, args) ← getUnifyKeyArgs e;
match k with
| Key.star => d.root.foldlM (fun result k c => getUnifyAux k.arity #[] c result) #[]

38
stage0/src/Init/Lean/Meta/ExprDefEq.lean
View file

@ -27,7 +27,7 @@ namespace Meta
private def isDefEqEta (a b : Expr) : MetaM Bool :=
if a.isLambda && !b.isLambda then do
bType ← inferType b;
bType ← whnfUsingDefault bType;
bType ← whnfD bType;
match bType with
| Expr.forallE n d _ c =>
let b' := Lean.mkLambda n c.binderInfo d (mkApp b (mkBVar 0));
@ -128,7 +128,7 @@ if h : args₁.size = args₂.size then do
synthPending a₂;
pure ()
};
usingAtLeastTransparency TransparencyMode.default $ isExprDefEqAux a₁ a₂)
withAtLeastTransparency TransparencyMode.default $ isExprDefEqAux a₁ a₂)
else
pure false
@ -628,6 +628,29 @@ private def simpAssignmentArg (arg : Expr) : MetaM Expr := do
arg ← if arg.getAppFn.hasExprMVar then instantiateMVars arg else pure arg;
simpAssignmentArgAux arg
private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
traceCtx `Meta.isDefEq.assign.checkTypes $ do
-- must check whether types are definitionally equal or not, before assigning and returning true
mvarType ← inferType mvar;
vType ← inferType v;
condM (withTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType)
(do assignExprMVar mvar.mvarId! v; pure true)
(do trace `Meta.isDefEq.assign.typeMismatch $ fun _ => mvar ++ " : " ++ mvarType ++ " := " ++ v ++ " : " ++ vType;
pure false)
private def processConstApprox (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool := do
let mvarId := mvar.mvarId!;
v? ← checkAssignment mvarId #[] v;
match v? with
| none => pure false
| some v => do
mvarDecl ← getMVarDecl mvarId;
forallBoundedTelescope mvarDecl.type numArgs $ fun xs _ =>
if xs.size != numArgs then pure false
else do
v ← mkLambda xs v;
checkTypesAndAssign mvar v
private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl) (v : Expr) : Nat → Array Expr → MetaM Bool
| i, args =>
if h : i < args.size then do
@ -636,8 +659,10 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
arg ← simpAssignmentArg arg;
let args := args.set ⟨i, h⟩ arg;
let useFOApprox : Unit → MetaM Bool := fun _ =>
if cfg.foApprox then
if cfg.foApprox && v.isApp then
processAssignmentFOApprox mvar args v
else if cfg.constApprox then
processConstApprox mvar args.size v
else
pure false;
match arg with
@ -654,6 +679,7 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
cfg ← getConfig;
v ← instantiateMVars v; -- enforce A4
if cfg.foApprox && args.isEmpty && v.getAppFn == mvar then
-- using A6
processAssignmentFOApprox mvar args v
else do
let useFOApprox : Unit → MetaM Bool := fun _ =>
@ -669,7 +695,7 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
-- must check whether types are definitionally equal or not, before assigning and returning true
mvarType ← inferType mvar;
vType ← inferType v;
condM (usingTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType)
condM (withTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType)
(do assignExprMVar mvarId v; pure true)
(do trace `Meta.isDefEq.assign.typeMismatch $ fun _ => mvar ++ " : " ++ mvarType ++ " := " ++ v ++ " : " ++ vType;
pure false)
@ -678,11 +704,11 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
/- We need to type check `v` because abstraction using `mkLambda` may have produced
a type incorrect term. See discussion at A2 -/
condM (isTypeCorrect v)
(finalize ())
(checkTypesAndAssign mvar v)
(do trace `Meta.isDefEq.assign.typeError $ fun _ => mvar ++ " := " ++ v;
useFOApprox ())
else
finalize ()
checkTypesAndAssign mvar v
/-- Tries to solve `?m a₁ ... aₙ =?= v` by assigning `?m`.
It assumes `?m` is unassigned. -/

2
stage0/src/Init/Lean/Meta/FunInfo.lean
View file

@ -56,7 +56,7 @@ else
private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
checkFunInfoCache fn maxArgs? $ do
fnType ← inferType fn;
usingTransparency TransparencyMode.default $
withTransparency TransparencyMode.default $
forallBoundedTelescope fnType maxArgs? $ fun fvars type => do
pinfo ← fvars.size.foldM
(fun (i : Nat) (pinfo : Array ParamInfo) => do

8
stage0/src/Init/Lean/Meta/InferType.lean
View file

@ -69,7 +69,7 @@ matchConst env structType.getAppFn failed $ fun structInfo structLvls => do
def getLevel (type : Expr) : MetaM Level := do
typeType ← inferType type;
typeType ← whnfUsingDefault typeType;
typeType ← whnfD typeType;
match typeType with
| Expr.sort lvl _ => pure lvl
| Expr.mvar mvarId _ =>
@ -141,7 +141,7 @@ private partial def inferTypeAux : Expr → MetaM Expr
| Expr.localE _ _ _ _ => unreachable!
def inferTypeImpl (e : Expr) : MetaM Expr :=
usingTransparency TransparencyMode.default (inferTypeAux e)
withTransparency TransparencyMode.default (inferTypeAux e)
@[init] def setInferTypeRef : IO Unit :=
inferTypeRef.set inferTypeImpl
@ -215,7 +215,7 @@ match r with
| LBool.undef => do
-- dbgTrace ("isPropQuick failed " ++ toString e);
type ← inferType e;
type ← whnfUsingDefault type;
type ← whnfD type;
match type with
| Expr.sort u _ => do u ← instantiateLevelMVars u; pure $ isAlwaysZero u
| _ => pure false
@ -323,7 +323,7 @@ match r with
| LBool.false => pure false
| LBool.undef => do
type ← inferType e;
type ← whnfUsingDefault type;
type ← whnfD type;
match type with
| Expr.sort _ _ => pure true
| _ => pure false

2
stage0/src/Init/Lean/Meta/SynthInstance.lean
View file

@ -511,7 +511,7 @@ try $
r.exprReplacements.allM (fun ⟨e, e'⟩ => isExprDefEqAux e e')
def synthInstance? (type : Expr) (fuel : Nat := 10000) : MetaM (Option Expr) :=
usingTransparency TransparencyMode.reducible $ do
withConfig (fun config => { transparency := TransparencyMode.reducible, foApprox := true, ctxApprox := true, .. config }) $ do
type ← instantiateMVars type;
type ← preprocess type;
s ← get;

14
stage0/src/runtime/lean.h
View file

@ -1434,12 +1434,22 @@ static inline bool lean_int_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
}
}
lean_obj_res lean_big_int_to_nat(lean_obj_arg a);
static inline lean_obj_res lean_int_to_nat(lean_obj_arg a) {
assert(!lean_int_lt(a, lean_box(0)));
if (lean_is_scalar(a)) {
return a;
} else {
return lean_big_int_to_nat(a);
}
}
static inline lean_obj_res lean_nat_abs(b_lean_obj_arg i) {
if (lean_int_lt(i, lean_box(0))) {
return lean_int_neg(i);
return lean_int_to_nat(lean_int_neg(i));
} else {
lean_inc(i);
return i;
return lean_int_to_nat(i);
}
}

7
stage0/src/runtime/object.cpp
View file

@ -1232,6 +1232,13 @@ static object * mpz_to_int(mpz const & m) {
return lean_box(static_cast<unsigned>(m.get_int()));
}
extern "C" lean_obj_res lean_big_int_to_nat(lean_obj_arg a) {
lean_assert(!lean_is_scalar(a));
mpz m = mpz_value(a);
lean_dec(a);
return mpz_to_nat(m);
}
extern "C" object * lean_cstr_to_int(char const * n) {
return mpz_to_int(mpz(n));
}

2
stage0/src/shell/CMakeLists.txt
View file

@ -140,7 +140,7 @@ add_test(lean_version2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --v)
endif()
add_test(lean_ghash1 "${CMAKE_CURRENT_BINARY_DIR}/lean" -g)
add_test(lean_ghash2 "${CMAKE_CURRENT_BINARY_DIR}/lean" --githash)
# add_test(lean_new_frontend "${LEAN_SOURCE_DIR}/../bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean")
add_test(lean_new_frontend "${LEAN_SOURCE_DIR}/../bin/lean" --new-frontend "${LEAN_SOURCE_DIR}/Init/Core.lean")
add_test(lean_unknown_option bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "-z")
add_test(lean_unknown_file1 bash "${LEAN_SOURCE_DIR}/cmake/check_failure.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" "boofoo.lean")
if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows"))

19
stage0/stdlib/Init/Lean/Elab/Command.c
View file

@ -91,7 +91,6 @@ lean_object* l_PersistentHashMap_insertAux___main___at_Lean_Elab_Command_addBuil
lean_object* l_Lean_Elab_getPos___at_Lean_Elab_Command_elabCommand___spec__3(lean_object*, lean_object*, lean_object*);
lean_object* lean_dbg_trace(lean_object*, lean_object*);
lean_object* lean_io_mk_ref(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Meta_ExprDefEq_17__processAssignmentAux___main___closed__8;
lean_object* l_Lean_Elab_Command_getUniverseNames___boxed(lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_registerBuiltinCommandElabAttr___closed__2;
@ -321,6 +320,7 @@ lean_object* l_Lean_Elab_Command_declareBuiltinCommandElab___closed__1;
lean_object* l_Lean_Elab_Command_CommandElabM_monadLog;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabMixfix___closed__3;
lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main___at_Lean_Elab_Command_addBuiltinCommandElab___spec__9(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Meta_ExprDefEq_17__checkTypesAndAssign___closed__8;
extern lean_object* l_Lean_AttributeImpl_inhabited___closed__6;
lean_object* l___private_Init_Lean_Elab_Command_8__checkEndHeader___main___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
@ -4389,14 +4389,15 @@ lean_dec(x_4);
x_9 = 1;
x_10 = 0;
x_11 = 1;
x_12 = lean_alloc_ctor(0, 1, 6);
x_12 = lean_alloc_ctor(0, 1, 7);
lean_ctor_set(x_12, 0, x_5);
lean_ctor_set_uint8(x_12, sizeof(void*)*1, x_9);
lean_ctor_set_uint8(x_12, sizeof(void*)*1 + 1, x_9);
lean_ctor_set_uint8(x_12, sizeof(void*)*1 + 2, x_9);
lean_ctor_set_uint8(x_12, sizeof(void*)*1 + 3, x_9);
lean_ctor_set_uint8(x_12, sizeof(void*)*1 + 4, x_10);
lean_ctor_set_uint8(x_12, sizeof(void*)*1 + 5, x_11);
lean_ctor_set_uint8(x_12, sizeof(void*)*1 + 3, x_10);
lean_ctor_set_uint8(x_12, sizeof(void*)*1 + 4, x_9);
lean_ctor_set_uint8(x_12, sizeof(void*)*1 + 5, x_10);
lean_ctor_set_uint8(x_12, sizeof(void*)*1 + 6, x_11);
x_13 = l_Lean_LocalContext_Inhabited___closed__2;
x_14 = l_Array_empty___closed__1;
x_15 = lean_alloc_ctor(0, 3, 0);
@ -13787,7 +13788,7 @@ lean_inc(x_93);
lean_dec(x_91);
x_94 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_94, 0, x_89);
x_95 = l___private_Init_Lean_Meta_ExprDefEq_17__processAssignmentAux___main___closed__8;
x_95 = l___private_Init_Lean_Meta_ExprDefEq_17__checkTypesAndAssign___closed__8;
x_96 = lean_alloc_ctor(8, 2, 0);
lean_ctor_set(x_96, 0, x_94);
lean_ctor_set(x_96, 1, x_95);
@ -13899,7 +13900,7 @@ lean_inc(x_125);
lean_dec(x_123);
x_126 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_126, 0, x_121);
x_127 = l___private_Init_Lean_Meta_ExprDefEq_17__processAssignmentAux___main___closed__8;
x_127 = l___private_Init_Lean_Meta_ExprDefEq_17__checkTypesAndAssign___closed__8;
x_128 = lean_alloc_ctor(8, 2, 0);
lean_ctor_set(x_128, 0, x_126);
lean_ctor_set(x_128, 1, x_127);
@ -14035,7 +14036,7 @@ lean_inc(x_207);
lean_dec(x_205);
x_208 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_208, 0, x_203);
x_209 = l___private_Init_Lean_Meta_ExprDefEq_17__processAssignmentAux___main___closed__8;
x_209 = l___private_Init_Lean_Meta_ExprDefEq_17__checkTypesAndAssign___closed__8;
x_210 = lean_alloc_ctor(8, 2, 0);
lean_ctor_set(x_210, 0, x_208);
lean_ctor_set(x_210, 1, x_209);
@ -14316,7 +14317,7 @@ lean_inc(x_279);
lean_dec(x_277);
x_280 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_280, 0, x_275);
x_281 = l___private_Init_Lean_Meta_ExprDefEq_17__processAssignmentAux___main___closed__8;
x_281 = l___private_Init_Lean_Meta_ExprDefEq_17__checkTypesAndAssign___closed__8;
x_282 = lean_alloc_ctor(8, 2, 0);
lean_ctor_set(x_282, 0, x_280);
lean_ctor_set(x_282, 1, x_281);

12
stage0/stdlib/Init/Lean/Meta/AppBuilder.c
View file

@ -90,7 +90,6 @@ lean_object* l_Lean_Expr_getRevArg_x21___main(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkFreshExprMVar(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkHEqSymm(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_whnfUsingDefault(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkApp5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkAppM___closed__1;
lean_object* l___private_Init_Lean_Meta_AppBuilder_3__mkAppMAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -112,6 +111,7 @@ lean_object* l_Lean_Expr_arrow_x3f___boxed(lean_object*);
lean_object* l_Lean_Meta_getMVarDecl(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_AppBuilder_3__mkAppMAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_whnfD(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkFreshLevelMVar___rarg(lean_object*);
lean_object* l_Lean_Meta_mkHEq(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkHEqTrans___closed__1;
@ -835,7 +835,7 @@ lean_inc(x_5);
x_6 = lean_ctor_get(x_4, 1);
lean_inc(x_6);
lean_dec(x_4);
x_7 = l_Lean_Meta_whnfUsingDefault(x_5, x_2, x_6);
x_7 = l_Lean_Meta_whnfD(x_5, x_2, x_6);
return x_7;
}
else
@ -3156,7 +3156,7 @@ lean_dec(x_32);
x_34 = l_Lean_Expr_getRevArg_x21___main(x_7, x_33);
lean_dec(x_7);
lean_inc(x_3);
x_35 = l_Lean_Meta_whnfUsingDefault(x_27, x_3, x_8);
x_35 = l_Lean_Meta_whnfD(x_27, x_3, x_8);
if (lean_obj_tag(x_35) == 0)
{
lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39;
@ -3444,7 +3444,7 @@ lean_dec(x_118);
x_120 = l_Lean_Expr_getRevArg_x21___main(x_92, x_119);
lean_dec(x_92);
lean_inc(x_3);
x_121 = l_Lean_Meta_whnfUsingDefault(x_113, x_3, x_93);
x_121 = l_Lean_Meta_whnfD(x_113, x_3, x_93);
if (lean_obj_tag(x_121) == 0)
{
lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125;
@ -3898,7 +3898,7 @@ x_36 = lean_ctor_get(x_30, 1);
lean_inc(x_36);
lean_dec(x_30);
lean_inc(x_3);
x_37 = l_Lean_Meta_whnfUsingDefault(x_31, x_3, x_10);
x_37 = l_Lean_Meta_whnfD(x_31, x_3, x_10);
if (lean_obj_tag(x_37) == 0)
{
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
@ -4812,7 +4812,7 @@ x_12 = lean_expr_instantiate_rev_range(x_7, x_5, x_11, x_4);
lean_dec(x_5);
lean_dec(x_7);
lean_inc(x_8);
x_13 = l_Lean_Meta_whnfUsingDefault(x_12, x_8, x_9);
x_13 = l_Lean_Meta_whnfD(x_12, x_8, x_9);
if (lean_obj_tag(x_13) == 0)
{
uint8_t x_14;

605
stage0/stdlib/Init/Lean/Meta/Basic.c
View file

@ -13,6 +13,7 @@
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Lean_Meta_withConfig___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_isClassExpensive___main___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_MetaM_inhabited(lean_object*, lean_object*);
size_t l_Lean_Meta_InfoCacheKey_Hashable(lean_object*);
@ -120,9 +121,9 @@ lean_object* l_Lean_Meta_withLocalDeclD(lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallBoundedTelescope___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getConst___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Meta_withTransparency___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at___private_Init_Lean_Meta_Basic_7__lambdaTelescopeAux___main___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_forallTelescopeReducing(lean_object*);
lean_object* l_Lean_Meta_usingAtLeastTransparency(lean_object*);
lean_object* l_Lean_Meta_MetaM_inhabited___rarg(lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_7__lambdaTelescopeAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_Hashable___closed__1;
@ -183,6 +184,7 @@ lean_object* l___private_Init_Lean_Meta_Basic_5__forallTelescopeReducingAuxAux__
lean_object* l_Lean_Meta_TransparencyMode_Hashable;
lean_object* l_Lean_Meta_dbgTrace___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
lean_object* l_Lean_Meta_withTransparency(lean_object*);
lean_object* l_Lean_Meta_tracer___closed__5;
lean_object* l___private_Init_Lean_Meta_Basic_5__forallTelescopeReducingAuxAux___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkSynthPendingRef___lambda__1(lean_object*, lean_object*, lean_object*);
@ -223,6 +225,7 @@ lean_object* l_Lean_Meta_withNewLocalInstances(lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main(lean_object*);
extern lean_object* l_Lean_Options_empty;
lean_object* l_Lean_Meta_approxDefEq___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withAtLeastTransparency___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_MetaExtState_inhabited___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescopeReducing___spec__4___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Meta_TransparencyMode_beq(uint8_t, uint8_t);
@ -256,9 +259,7 @@ uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
lean_object* l_Lean_Meta_liftStateMCtx___rarg(lean_object*, lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Lean_Meta_mkMetaExtension___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Meta_usingTransparency(lean_object*);
lean_object* l_Lean_Meta_withLocalDecl___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_usingAtLeastTransparency___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescopeReducing___spec__4___rarg___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_isClassExpensive___main___spec__5(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLevelMVar(lean_object*);
@ -300,11 +301,10 @@ lean_object* l_Lean_Meta_liftStateMCtx___rarg___boxed(lean_object*, lean_object*
lean_object* l_Lean_Meta_tracer___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_resettingSynthInstanceCache(lean_object*);
lean_object* l_Lean_Meta_mkFreshExprMVar(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Meta_usingAtLeastTransparency___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_8__forallMetaTelescopeReducingAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_hasMVar(lean_object*);
lean_object* l_Lean_Meta_whnfUsingDefault(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_tracer___closed__2;
lean_object* l_Lean_Meta_withAtLeastTransparency___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* lean_metavar_ctx_mk_decl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_Meta_synthPendingRef;
lean_object* l_Lean_Meta_getConstAux(lean_object*, uint8_t, lean_object*, lean_object*);
@ -333,9 +333,9 @@ lean_object* l_Lean_Meta_mkFreshExprMVar___boxed(lean_object*, lean_object*, lea
lean_object* l_Lean_Meta_isReducible(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerEnvExtensionUnsafe___rarg___closed__2;
lean_object* l_Lean_Meta_withNewLocalInstances___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withAtLeastTransparency(lean_object*);
lean_object* l_Lean_Meta_dbgTrace(lean_object*);
lean_object* l_Lean_Meta_mkFreshId(lean_object*);
lean_object* l_Lean_Meta_usingTransparency___rarg(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_5__forallTelescopeReducingAuxAux___main___at_Lean_Meta_forallBoundedTelescope___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_beq___boxed(lean_object*, lean_object*);
@ -367,6 +367,7 @@ lean_object* l_Lean_Meta_forallMetaTelescope(lean_object*, lean_object*, lean_ob
lean_object* l_Lean_Meta_isClassQuickConst(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_EnvExtension_getStateUnsafe___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_MetaExtState_inhabited;
lean_object* l_Lean_Meta_withConfig(lean_object*);
lean_object* l_Lean_Meta_withNewMCtxDepth(lean_object*);
lean_object* l_Lean_Meta_shouldReduceReducibleOnly(lean_object*, lean_object*);
lean_object* l_Lean_Meta_getMCtx___rarg(lean_object*);
@ -406,7 +407,6 @@ lean_object* l_Lean_Meta_mkWHNFRef___lambda__1(lean_object*, lean_object*, lean_
lean_object* l_Lean_Meta_withNewLocalInstance(lean_object*);
lean_object* l_Lean_Meta_mkWHNFRef(lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_1__whenDebugging(lean_object*);
lean_object* l_Lean_Meta_usingTransparency___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_local_ctx_find(lean_object*, lean_object*);
lean_object* l_Lean_MetavarContext_MkBinding_mkBinding___at_Lean_MetavarContext_mkBinding___spec__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getConfig(lean_object*, lean_object*);
@ -436,6 +436,7 @@ lean_object* l_Lean_Meta_getConstAux___boxed(lean_object*, lean_object*, lean_ob
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_isClassExpensive___main___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getFVarLocalDecl(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallBoundedTelescope___spec__3(lean_object*);
lean_object* l_Lean_Meta_withTransparency___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t _init_l_Lean_Meta_TransparencyMode_Inhabited() {
_start:
{
@ -2380,7 +2381,7 @@ _start:
lean_object* x_4; uint8_t x_5;
x_4 = lean_ctor_get(x_2, 0);
lean_inc(x_4);
x_5 = lean_ctor_get_uint8(x_4, sizeof(void*)*1 + 4);
x_5 = lean_ctor_get_uint8(x_4, sizeof(void*)*1 + 5);
lean_dec(x_4);
if (x_5 == 0)
{
@ -2461,7 +2462,7 @@ _start:
{
lean_object* x_3; uint8_t x_4; uint8_t x_5; uint8_t x_6; lean_object* x_7; lean_object* x_8;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get_uint8(x_3, sizeof(void*)*1 + 5);
x_4 = lean_ctor_get_uint8(x_3, sizeof(void*)*1 + 6);
x_5 = 0;
x_6 = l_Lean_Meta_TransparencyMode_beq(x_4, x_5);
x_7 = lean_box(x_6);
@ -2485,7 +2486,7 @@ _start:
{
lean_object* x_3; uint8_t x_4; uint8_t x_5; uint8_t x_6; lean_object* x_7; lean_object* x_8;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get_uint8(x_3, sizeof(void*)*1 + 5);
x_4 = lean_ctor_get_uint8(x_3, sizeof(void*)*1 + 6);
x_5 = 2;
x_6 = l_Lean_Meta_TransparencyMode_beq(x_4, x_5);
x_7 = lean_box(x_6);
@ -2509,7 +2510,7 @@ _start:
{
lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get_uint8(x_3, sizeof(void*)*1 + 5);
x_4 = lean_ctor_get_uint8(x_3, sizeof(void*)*1 + 6);
x_5 = lean_box(x_4);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_5);
@ -2571,7 +2572,49 @@ lean_dec(x_2);
return x_4;
}
}
lean_object* l_Lean_Meta_usingTransparency___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Meta_withConfig___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
x_5 = !lean_is_exclusive(x_3);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = lean_ctor_get(x_3, 0);
x_7 = lean_apply_1(x_1, x_6);
lean_ctor_set(x_3, 0, x_7);
x_8 = lean_apply_2(x_2, x_3, x_4);
return x_8;
}
else
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_9 = lean_ctor_get(x_3, 0);
x_10 = lean_ctor_get(x_3, 1);
x_11 = lean_ctor_get(x_3, 2);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_dec(x_3);
x_12 = lean_apply_1(x_1, x_9);
x_13 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_13, 0, x_12);
lean_ctor_set(x_13, 1, x_10);
lean_ctor_set(x_13, 2, x_11);
x_14 = lean_apply_2(x_2, x_13, x_4);
return x_14;
}
}
}
lean_object* l_Lean_Meta_withConfig(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Meta_withConfig___rarg), 4, 0);
return x_2;
}
}
lean_object* l_Lean_Meta_withTransparency___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
@ -2584,98 +2627,102 @@ x_7 = !lean_is_exclusive(x_6);
if (x_7 == 0)
{
lean_object* x_8;
lean_ctor_set_uint8(x_6, sizeof(void*)*1 + 5, x_1);
lean_ctor_set_uint8(x_6, sizeof(void*)*1 + 6, x_1);
x_8 = lean_apply_2(x_2, x_3, x_4);
return x_8;
}
else
{
lean_object* x_9; uint8_t x_10; uint8_t x_11; uint8_t x_12; uint8_t x_13; uint8_t x_14; lean_object* x_15; lean_object* x_16;
lean_object* x_9; uint8_t x_10; uint8_t x_11; uint8_t x_12; uint8_t x_13; uint8_t x_14; uint8_t x_15; lean_object* x_16; lean_object* x_17;
x_9 = lean_ctor_get(x_6, 0);
x_10 = lean_ctor_get_uint8(x_6, sizeof(void*)*1);
x_11 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 1);
x_12 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 2);
x_13 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 3);
x_14 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 4);
x_15 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 5);
lean_inc(x_9);
lean_dec(x_6);
x_15 = lean_alloc_ctor(0, 1, 6);
lean_ctor_set(x_15, 0, x_9);
lean_ctor_set_uint8(x_15, sizeof(void*)*1, x_10);
lean_ctor_set_uint8(x_15, sizeof(void*)*1 + 1, x_11);
lean_ctor_set_uint8(x_15, sizeof(void*)*1 + 2, x_12);
lean_ctor_set_uint8(x_15, sizeof(void*)*1 + 3, x_13);
lean_ctor_set_uint8(x_15, sizeof(void*)*1 + 4, x_14);
lean_ctor_set_uint8(x_15, sizeof(void*)*1 + 5, x_1);
lean_ctor_set(x_3, 0, x_15);
x_16 = lean_apply_2(x_2, x_3, x_4);
return x_16;
x_16 = lean_alloc_ctor(0, 1, 7);
lean_ctor_set(x_16, 0, x_9);
lean_ctor_set_uint8(x_16, sizeof(void*)*1, x_10);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 1, x_11);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 2, x_12);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 3, x_13);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 4, x_14);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 5, x_15);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 6, x_1);
lean_ctor_set(x_3, 0, x_16);
x_17 = lean_apply_2(x_2, x_3, x_4);
return x_17;
}
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t x_21; uint8_t x_22; uint8_t x_23; uint8_t x_24; uint8_t x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_17 = lean_ctor_get(x_3, 0);
x_18 = lean_ctor_get(x_3, 1);
x_19 = lean_ctor_get(x_3, 2);
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; uint8_t x_23; uint8_t x_24; uint8_t x_25; uint8_t x_26; uint8_t x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_18 = lean_ctor_get(x_3, 0);
x_19 = lean_ctor_get(x_3, 1);
x_20 = lean_ctor_get(x_3, 2);
lean_inc(x_20);
lean_inc(x_19);
lean_inc(x_18);
lean_inc(x_17);
lean_dec(x_3);
x_20 = lean_ctor_get(x_17, 0);
lean_inc(x_20);
x_21 = lean_ctor_get_uint8(x_17, sizeof(void*)*1);
x_22 = lean_ctor_get_uint8(x_17, sizeof(void*)*1 + 1);
x_23 = lean_ctor_get_uint8(x_17, sizeof(void*)*1 + 2);
x_24 = lean_ctor_get_uint8(x_17, sizeof(void*)*1 + 3);
x_25 = lean_ctor_get_uint8(x_17, sizeof(void*)*1 + 4);
if (lean_is_exclusive(x_17)) {
lean_ctor_release(x_17, 0);
x_26 = x_17;
x_21 = lean_ctor_get(x_18, 0);
lean_inc(x_21);
x_22 = lean_ctor_get_uint8(x_18, sizeof(void*)*1);
x_23 = lean_ctor_get_uint8(x_18, sizeof(void*)*1 + 1);
x_24 = lean_ctor_get_uint8(x_18, sizeof(void*)*1 + 2);
x_25 = lean_ctor_get_uint8(x_18, sizeof(void*)*1 + 3);
x_26 = lean_ctor_get_uint8(x_18, sizeof(void*)*1 + 4);
x_27 = lean_ctor_get_uint8(x_18, sizeof(void*)*1 + 5);
if (lean_is_exclusive(x_18)) {
lean_ctor_release(x_18, 0);
x_28 = x_18;
} else {
lean_dec_ref(x_17);
x_26 = lean_box(0);
lean_dec_ref(x_18);
x_28 = lean_box(0);
}
if (lean_is_scalar(x_26)) {
x_27 = lean_alloc_ctor(0, 1, 6);
if (lean_is_scalar(x_28)) {
x_29 = lean_alloc_ctor(0, 1, 7);
} else {
x_27 = x_26;
x_29 = x_28;
}
lean_ctor_set(x_27, 0, x_20);
lean_ctor_set_uint8(x_27, sizeof(void*)*1, x_21);
lean_ctor_set_uint8(x_27, sizeof(void*)*1 + 1, x_22);
lean_ctor_set_uint8(x_27, sizeof(void*)*1 + 2, x_23);
lean_ctor_set_uint8(x_27, sizeof(void*)*1 + 3, x_24);
lean_ctor_set_uint8(x_27, sizeof(void*)*1 + 4, x_25);
lean_ctor_set_uint8(x_27, sizeof(void*)*1 + 5, x_1);
x_28 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_28, 0, x_27);
lean_ctor_set(x_28, 1, x_18);
lean_ctor_set(x_28, 2, x_19);
x_29 = lean_apply_2(x_2, x_28, x_4);
return x_29;
lean_ctor_set(x_29, 0, x_21);
lean_ctor_set_uint8(x_29, sizeof(void*)*1, x_22);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 1, x_23);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 2, x_24);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 3, x_25);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 4, x_26);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 5, x_27);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 6, x_1);
x_30 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_30, 0, x_29);
lean_ctor_set(x_30, 1, x_19);
lean_ctor_set(x_30, 2, x_20);
x_31 = lean_apply_2(x_2, x_30, x_4);
return x_31;
}
}
}
lean_object* l_Lean_Meta_usingTransparency(lean_object* x_1) {
lean_object* l_Lean_Meta_withTransparency(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Meta_usingTransparency___rarg___boxed), 4, 0);
x_2 = lean_alloc_closure((void*)(l_Lean_Meta_withTransparency___rarg___boxed), 4, 0);
return x_2;
}
}
lean_object* l_Lean_Meta_usingTransparency___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Meta_withTransparency___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5; lean_object* x_6;
x_5 = lean_unbox(x_1);
lean_dec(x_1);
x_6 = l_Lean_Meta_usingTransparency___rarg(x_5, x_2, x_3, x_4);
x_6 = l_Lean_Meta_withTransparency___rarg(x_5, x_2, x_3, x_4);
return x_6;
}
}
lean_object* l_Lean_Meta_usingAtLeastTransparency___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Meta_withAtLeastTransparency___rarg(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
@ -2688,7 +2735,7 @@ x_7 = !lean_is_exclusive(x_6);
if (x_7 == 0)
{
uint8_t x_8; uint8_t x_9;
x_8 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 5);
x_8 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 6);
x_9 = l_Lean_Meta_TransparencyMode_lt(x_8, x_1);
if (x_9 == 0)
{
@ -2699,14 +2746,14 @@ return x_10;
else
{
lean_object* x_11;
lean_ctor_set_uint8(x_6, sizeof(void*)*1 + 5, x_1);
lean_ctor_set_uint8(x_6, sizeof(void*)*1 + 6, x_1);
x_11 = lean_apply_2(x_2, x_3, x_4);
return x_11;
}
}
else
{
lean_object* x_12; uint8_t x_13; uint8_t x_14; uint8_t x_15; uint8_t x_16; uint8_t x_17; uint8_t x_18; uint8_t x_19;
lean_object* x_12; uint8_t x_13; uint8_t x_14; uint8_t x_15; uint8_t x_16; uint8_t x_17; uint8_t x_18; uint8_t x_19; uint8_t x_20;
x_12 = lean_ctor_get(x_6, 0);
x_13 = lean_ctor_get_uint8(x_6, sizeof(void*)*1);
x_14 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 1);
@ -2714,129 +2761,135 @@ x_15 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 2);
x_16 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 3);
x_17 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 4);
x_18 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 5);
x_19 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 6);
lean_inc(x_12);
lean_dec(x_6);
x_19 = l_Lean_Meta_TransparencyMode_lt(x_18, x_1);
if (x_19 == 0)
x_20 = l_Lean_Meta_TransparencyMode_lt(x_19, x_1);
if (x_20 == 0)
{
lean_object* x_20; lean_object* x_21;
x_20 = lean_alloc_ctor(0, 1, 6);
lean_ctor_set(x_20, 0, x_12);
lean_ctor_set_uint8(x_20, sizeof(void*)*1, x_13);
lean_ctor_set_uint8(x_20, sizeof(void*)*1 + 1, x_14);
lean_ctor_set_uint8(x_20, sizeof(void*)*1 + 2, x_15);
lean_ctor_set_uint8(x_20, sizeof(void*)*1 + 3, x_16);
lean_ctor_set_uint8(x_20, sizeof(void*)*1 + 4, x_17);
lean_ctor_set_uint8(x_20, sizeof(void*)*1 + 5, x_18);
lean_ctor_set(x_3, 0, x_20);
x_21 = lean_apply_2(x_2, x_3, x_4);
return x_21;
lean_object* x_21; lean_object* x_22;
x_21 = lean_alloc_ctor(0, 1, 7);
lean_ctor_set(x_21, 0, x_12);
lean_ctor_set_uint8(x_21, sizeof(void*)*1, x_13);
lean_ctor_set_uint8(x_21, sizeof(void*)*1 + 1, x_14);
lean_ctor_set_uint8(x_21, sizeof(void*)*1 + 2, x_15);
lean_ctor_set_uint8(x_21, sizeof(void*)*1 + 3, x_16);
lean_ctor_set_uint8(x_21, sizeof(void*)*1 + 4, x_17);
lean_ctor_set_uint8(x_21, sizeof(void*)*1 + 5, x_18);
lean_ctor_set_uint8(x_21, sizeof(void*)*1 + 6, x_19);
lean_ctor_set(x_3, 0, x_21);
x_22 = lean_apply_2(x_2, x_3, x_4);
return x_22;
}
else
{
lean_object* x_22; lean_object* x_23;
x_22 = lean_alloc_ctor(0, 1, 6);
lean_ctor_set(x_22, 0, x_12);
lean_ctor_set_uint8(x_22, sizeof(void*)*1, x_13);
lean_ctor_set_uint8(x_22, sizeof(void*)*1 + 1, x_14);
lean_ctor_set_uint8(x_22, sizeof(void*)*1 + 2, x_15);
lean_ctor_set_uint8(x_22, sizeof(void*)*1 + 3, x_16);
lean_ctor_set_uint8(x_22, sizeof(void*)*1 + 4, x_17);
lean_ctor_set_uint8(x_22, sizeof(void*)*1 + 5, x_1);
lean_ctor_set(x_3, 0, x_22);
x_23 = lean_apply_2(x_2, x_3, x_4);
return x_23;
lean_object* x_23; lean_object* x_24;
x_23 = lean_alloc_ctor(0, 1, 7);
lean_ctor_set(x_23, 0, x_12);
lean_ctor_set_uint8(x_23, sizeof(void*)*1, x_13);
lean_ctor_set_uint8(x_23, sizeof(void*)*1 + 1, x_14);
lean_ctor_set_uint8(x_23, sizeof(void*)*1 + 2, x_15);
lean_ctor_set_uint8(x_23, sizeof(void*)*1 + 3, x_16);
lean_ctor_set_uint8(x_23, sizeof(void*)*1 + 4, x_17);
lean_ctor_set_uint8(x_23, sizeof(void*)*1 + 5, x_18);
lean_ctor_set_uint8(x_23, sizeof(void*)*1 + 6, x_1);
lean_ctor_set(x_3, 0, x_23);
x_24 = lean_apply_2(x_2, x_3, x_4);
return x_24;
}
}
}
else
{
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; uint8_t x_28; uint8_t x_29; uint8_t x_30; uint8_t x_31; uint8_t x_32; uint8_t x_33; lean_object* x_34; uint8_t x_35;
x_24 = lean_ctor_get(x_3, 0);
x_25 = lean_ctor_get(x_3, 1);
x_26 = lean_ctor_get(x_3, 2);
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; uint8_t x_29; uint8_t x_30; uint8_t x_31; uint8_t x_32; uint8_t x_33; uint8_t x_34; uint8_t x_35; lean_object* x_36; uint8_t x_37;
x_25 = lean_ctor_get(x_3, 0);
x_26 = lean_ctor_get(x_3, 1);
x_27 = lean_ctor_get(x_3, 2);
lean_inc(x_27);
lean_inc(x_26);
lean_inc(x_25);
lean_inc(x_24);
lean_dec(x_3);
x_27 = lean_ctor_get(x_24, 0);
lean_inc(x_27);
x_28 = lean_ctor_get_uint8(x_24, sizeof(void*)*1);
x_29 = lean_ctor_get_uint8(x_24, sizeof(void*)*1 + 1);
x_30 = lean_ctor_get_uint8(x_24, sizeof(void*)*1 + 2);
x_31 = lean_ctor_get_uint8(x_24, sizeof(void*)*1 + 3);
x_32 = lean_ctor_get_uint8(x_24, sizeof(void*)*1 + 4);
x_33 = lean_ctor_get_uint8(x_24, sizeof(void*)*1 + 5);
if (lean_is_exclusive(x_24)) {
lean_ctor_release(x_24, 0);
x_34 = x_24;
x_28 = lean_ctor_get(x_25, 0);
lean_inc(x_28);
x_29 = lean_ctor_get_uint8(x_25, sizeof(void*)*1);
x_30 = lean_ctor_get_uint8(x_25, sizeof(void*)*1 + 1);
x_31 = lean_ctor_get_uint8(x_25, sizeof(void*)*1 + 2);
x_32 = lean_ctor_get_uint8(x_25, sizeof(void*)*1 + 3);
x_33 = lean_ctor_get_uint8(x_25, sizeof(void*)*1 + 4);
x_34 = lean_ctor_get_uint8(x_25, sizeof(void*)*1 + 5);
x_35 = lean_ctor_get_uint8(x_25, sizeof(void*)*1 + 6);
if (lean_is_exclusive(x_25)) {
lean_ctor_release(x_25, 0);
x_36 = x_25;
} else {
lean_dec_ref(x_24);
x_34 = lean_box(0);
lean_dec_ref(x_25);
x_36 = lean_box(0);
}
x_35 = l_Lean_Meta_TransparencyMode_lt(x_33, x_1);
if (x_35 == 0)
x_37 = l_Lean_Meta_TransparencyMode_lt(x_35, x_1);
if (x_37 == 0)
{
lean_object* x_36; lean_object* x_37; lean_object* x_38;
if (lean_is_scalar(x_34)) {
x_36 = lean_alloc_ctor(0, 1, 6);
lean_object* x_38; lean_object* x_39; lean_object* x_40;
if (lean_is_scalar(x_36)) {
x_38 = lean_alloc_ctor(0, 1, 7);
} else {
x_36 = x_34;
x_38 = x_36;
}
lean_ctor_set(x_36, 0, x_27);
lean_ctor_set_uint8(x_36, sizeof(void*)*1, x_28);
lean_ctor_set_uint8(x_36, sizeof(void*)*1 + 1, x_29);
lean_ctor_set_uint8(x_36, sizeof(void*)*1 + 2, x_30);
lean_ctor_set_uint8(x_36, sizeof(void*)*1 + 3, x_31);
lean_ctor_set_uint8(x_36, sizeof(void*)*1 + 4, x_32);
lean_ctor_set_uint8(x_36, sizeof(void*)*1 + 5, x_33);
x_37 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_37, 0, x_36);
lean_ctor_set(x_37, 1, x_25);
lean_ctor_set(x_37, 2, x_26);
x_38 = lean_apply_2(x_2, x_37, x_4);
return x_38;
lean_ctor_set(x_38, 0, x_28);
lean_ctor_set_uint8(x_38, sizeof(void*)*1, x_29);
lean_ctor_set_uint8(x_38, sizeof(void*)*1 + 1, x_30);
lean_ctor_set_uint8(x_38, sizeof(void*)*1 + 2, x_31);
lean_ctor_set_uint8(x_38, sizeof(void*)*1 + 3, x_32);
lean_ctor_set_uint8(x_38, sizeof(void*)*1 + 4, x_33);
lean_ctor_set_uint8(x_38, sizeof(void*)*1 + 5, x_34);
lean_ctor_set_uint8(x_38, sizeof(void*)*1 + 6, x_35);
x_39 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_39, 0, x_38);
lean_ctor_set(x_39, 1, x_26);
lean_ctor_set(x_39, 2, x_27);
x_40 = lean_apply_2(x_2, x_39, x_4);
return x_40;
}
else
{
lean_object* x_39; lean_object* x_40; lean_object* x_41;
if (lean_is_scalar(x_34)) {
x_39 = lean_alloc_ctor(0, 1, 6);
lean_object* x_41; lean_object* x_42; lean_object* x_43;
if (lean_is_scalar(x_36)) {
x_41 = lean_alloc_ctor(0, 1, 7);
} else {
x_39 = x_34;
x_41 = x_36;
}
lean_ctor_set(x_39, 0, x_27);
lean_ctor_set_uint8(x_39, sizeof(void*)*1, x_28);
lean_ctor_set_uint8(x_39, sizeof(void*)*1 + 1, x_29);
lean_ctor_set_uint8(x_39, sizeof(void*)*1 + 2, x_30);
lean_ctor_set_uint8(x_39, sizeof(void*)*1 + 3, x_31);
lean_ctor_set_uint8(x_39, sizeof(void*)*1 + 4, x_32);
lean_ctor_set_uint8(x_39, sizeof(void*)*1 + 5, x_1);
x_40 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_25);
lean_ctor_set(x_40, 2, x_26);
x_41 = lean_apply_2(x_2, x_40, x_4);
return x_41;
lean_ctor_set(x_41, 0, x_28);
lean_ctor_set_uint8(x_41, sizeof(void*)*1, x_29);
lean_ctor_set_uint8(x_41, sizeof(void*)*1 + 1, x_30);
lean_ctor_set_uint8(x_41, sizeof(void*)*1 + 2, x_31);
lean_ctor_set_uint8(x_41, sizeof(void*)*1 + 3, x_32);
lean_ctor_set_uint8(x_41, sizeof(void*)*1 + 4, x_33);
lean_ctor_set_uint8(x_41, sizeof(void*)*1 + 5, x_34);
lean_ctor_set_uint8(x_41, sizeof(void*)*1 + 6, x_1);
x_42 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_42, 0, x_41);
lean_ctor_set(x_42, 1, x_26);
lean_ctor_set(x_42, 2, x_27);
x_43 = lean_apply_2(x_2, x_42, x_4);
return x_43;
}
}
}
}
lean_object* l_Lean_Meta_usingAtLeastTransparency(lean_object* x_1) {
lean_object* l_Lean_Meta_withAtLeastTransparency(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Meta_usingAtLeastTransparency___rarg___boxed), 4, 0);
x_2 = lean_alloc_closure((void*)(l_Lean_Meta_withAtLeastTransparency___rarg___boxed), 4, 0);
return x_2;
}
}
lean_object* l_Lean_Meta_usingAtLeastTransparency___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Meta_withAtLeastTransparency___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5; lean_object* x_6;
x_5 = lean_unbox(x_1);
lean_dec(x_1);
x_6 = l_Lean_Meta_usingAtLeastTransparency___rarg(x_5, x_2, x_3, x_4);
x_6 = l_Lean_Meta_withAtLeastTransparency___rarg(x_5, x_2, x_3, x_4);
return x_6;
}
}
@ -3189,7 +3242,7 @@ _start:
{
lean_object* x_5; lean_object* x_22; uint8_t x_23;
x_22 = lean_ctor_get(x_3, 0);
x_23 = lean_ctor_get_uint8(x_22, sizeof(void*)*1 + 4);
x_23 = lean_ctor_get_uint8(x_22, sizeof(void*)*1 + 5);
if (x_23 == 0)
{
x_5 = x_4;
@ -3592,7 +3645,7 @@ case 1:
lean_object* x_14; uint8_t x_15; uint8_t x_16; uint8_t x_17;
lean_dec(x_13);
x_14 = lean_ctor_get(x_3, 0);
x_15 = lean_ctor_get_uint8(x_14, sizeof(void*)*1 + 5);
x_15 = lean_ctor_get_uint8(x_14, sizeof(void*)*1 + 6);
x_16 = 2;
x_17 = l_Lean_Meta_TransparencyMode_beq(x_15, x_16);
if (x_17 == 0)
@ -3636,7 +3689,7 @@ lean_dec(x_13);
lean_dec(x_5);
lean_dec(x_1);
x_23 = lean_ctor_get(x_3, 0);
x_24 = lean_ctor_get_uint8(x_23, sizeof(void*)*1 + 5);
x_24 = lean_ctor_get_uint8(x_23, sizeof(void*)*1 + 6);
x_25 = 0;
x_26 = l_Lean_Meta_TransparencyMode_beq(x_24, x_25);
if (x_26 == 0)
@ -16854,78 +16907,82 @@ if (x_7 == 0)
{
uint8_t x_8; lean_object* x_9;
x_8 = 2;
lean_ctor_set_uint8(x_6, sizeof(void*)*1 + 5, x_8);
lean_ctor_set_uint8(x_6, sizeof(void*)*1 + 6, x_8);
x_9 = l___private_Init_Lean_Meta_Basic_6__forallTelescopeReducingAux___at_Lean_Meta_isClassExpensive___main___spec__1(x_1, x_4, x_2, x_3);
return x_9;
}
else
{
lean_object* x_10; uint8_t x_11; uint8_t x_12; uint8_t x_13; uint8_t x_14; uint8_t x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18;
lean_object* x_10; uint8_t x_11; uint8_t x_12; uint8_t x_13; uint8_t x_14; uint8_t x_15; uint8_t x_16; uint8_t x_17; lean_object* x_18; lean_object* x_19;
x_10 = lean_ctor_get(x_6, 0);
x_11 = lean_ctor_get_uint8(x_6, sizeof(void*)*1);
x_12 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 1);
x_13 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 2);
x_14 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 3);
x_15 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 4);
x_16 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 5);
lean_inc(x_10);
lean_dec(x_6);
x_16 = 2;
x_17 = lean_alloc_ctor(0, 1, 6);
lean_ctor_set(x_17, 0, x_10);
lean_ctor_set_uint8(x_17, sizeof(void*)*1, x_11);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 1, x_12);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 2, x_13);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 3, x_14);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 4, x_15);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 5, x_16);
lean_ctor_set(x_2, 0, x_17);
x_18 = l___private_Init_Lean_Meta_Basic_6__forallTelescopeReducingAux___at_Lean_Meta_isClassExpensive___main___spec__1(x_1, x_4, x_2, x_3);
return x_18;
x_17 = 2;
x_18 = lean_alloc_ctor(0, 1, 7);
lean_ctor_set(x_18, 0, x_10);
lean_ctor_set_uint8(x_18, sizeof(void*)*1, x_11);
lean_ctor_set_uint8(x_18, sizeof(void*)*1 + 1, x_12);
lean_ctor_set_uint8(x_18, sizeof(void*)*1 + 2, x_13);
lean_ctor_set_uint8(x_18, sizeof(void*)*1 + 3, x_14);
lean_ctor_set_uint8(x_18, sizeof(void*)*1 + 4, x_15);
lean_ctor_set_uint8(x_18, sizeof(void*)*1 + 5, x_16);
lean_ctor_set_uint8(x_18, sizeof(void*)*1 + 6, x_17);
lean_ctor_set(x_2, 0, x_18);
x_19 = l___private_Init_Lean_Meta_Basic_6__forallTelescopeReducingAux___at_Lean_Meta_isClassExpensive___main___spec__1(x_1, x_4, x_2, x_3);
return x_19;
}
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; uint8_t x_24; uint8_t x_25; uint8_t x_26; uint8_t x_27; lean_object* x_28; uint8_t x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_19 = lean_ctor_get(x_2, 0);
x_20 = lean_ctor_get(x_2, 1);
x_21 = lean_ctor_get(x_2, 2);
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24; uint8_t x_25; uint8_t x_26; uint8_t x_27; uint8_t x_28; uint8_t x_29; lean_object* x_30; uint8_t x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34;
x_20 = lean_ctor_get(x_2, 0);
x_21 = lean_ctor_get(x_2, 1);
x_22 = lean_ctor_get(x_2, 2);
lean_inc(x_22);
lean_inc(x_21);
lean_inc(x_20);
lean_inc(x_19);
lean_dec(x_2);
x_22 = lean_ctor_get(x_19, 0);
lean_inc(x_22);
x_23 = lean_ctor_get_uint8(x_19, sizeof(void*)*1);
x_24 = lean_ctor_get_uint8(x_19, sizeof(void*)*1 + 1);
x_25 = lean_ctor_get_uint8(x_19, sizeof(void*)*1 + 2);
x_26 = lean_ctor_get_uint8(x_19, sizeof(void*)*1 + 3);
x_27 = lean_ctor_get_uint8(x_19, sizeof(void*)*1 + 4);
if (lean_is_exclusive(x_19)) {
lean_ctor_release(x_19, 0);
x_28 = x_19;
x_23 = lean_ctor_get(x_20, 0);
lean_inc(x_23);
x_24 = lean_ctor_get_uint8(x_20, sizeof(void*)*1);
x_25 = lean_ctor_get_uint8(x_20, sizeof(void*)*1 + 1);
x_26 = lean_ctor_get_uint8(x_20, sizeof(void*)*1 + 2);
x_27 = lean_ctor_get_uint8(x_20, sizeof(void*)*1 + 3);
x_28 = lean_ctor_get_uint8(x_20, sizeof(void*)*1 + 4);
x_29 = lean_ctor_get_uint8(x_20, sizeof(void*)*1 + 5);
if (lean_is_exclusive(x_20)) {
lean_ctor_release(x_20, 0);
x_30 = x_20;
} else {
lean_dec_ref(x_19);
x_28 = lean_box(0);
lean_dec_ref(x_20);
x_30 = lean_box(0);
}
x_29 = 2;
if (lean_is_scalar(x_28)) {
x_30 = lean_alloc_ctor(0, 1, 6);
x_31 = 2;
if (lean_is_scalar(x_30)) {
x_32 = lean_alloc_ctor(0, 1, 7);
} else {
x_30 = x_28;
x_32 = x_30;
}
lean_ctor_set(x_30, 0, x_22);
lean_ctor_set_uint8(x_30, sizeof(void*)*1, x_23);
lean_ctor_set_uint8(x_30, sizeof(void*)*1 + 1, x_24);
lean_ctor_set_uint8(x_30, sizeof(void*)*1 + 2, x_25);
lean_ctor_set_uint8(x_30, sizeof(void*)*1 + 3, x_26);
lean_ctor_set_uint8(x_30, sizeof(void*)*1 + 4, x_27);
lean_ctor_set_uint8(x_30, sizeof(void*)*1 + 5, x_29);
x_31 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_20);
lean_ctor_set(x_31, 2, x_21);
x_32 = l___private_Init_Lean_Meta_Basic_6__forallTelescopeReducingAux___at_Lean_Meta_isClassExpensive___main___spec__1(x_1, x_4, x_31, x_3);
return x_32;
lean_ctor_set(x_32, 0, x_23);
lean_ctor_set_uint8(x_32, sizeof(void*)*1, x_24);
lean_ctor_set_uint8(x_32, sizeof(void*)*1 + 1, x_25);
lean_ctor_set_uint8(x_32, sizeof(void*)*1 + 2, x_26);
lean_ctor_set_uint8(x_32, sizeof(void*)*1 + 3, x_27);
lean_ctor_set_uint8(x_32, sizeof(void*)*1 + 4, x_28);
lean_ctor_set_uint8(x_32, sizeof(void*)*1 + 5, x_29);
lean_ctor_set_uint8(x_32, sizeof(void*)*1 + 6, x_31);
x_33 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_21);
lean_ctor_set(x_33, 2, x_22);
x_34 = l___private_Init_Lean_Meta_Basic_6__forallTelescopeReducingAux___at_Lean_Meta_isClassExpensive___main___spec__1(x_1, x_4, x_33, x_3);
return x_34;
}
}
}
@ -40589,7 +40646,7 @@ lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Meta_whnfUsingDefault(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Meta_whnfD(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
@ -40603,89 +40660,85 @@ if (x_6 == 0)
{
uint8_t x_7; lean_object* x_8;
x_7 = 1;
lean_ctor_set_uint8(x_5, sizeof(void*)*1 + 5, x_7);
lean_ctor_set_uint8(x_5, sizeof(void*)*1 + 6, x_7);
x_8 = l_Lean_Meta_whnf(x_1, x_2, x_3);
return x_8;
}
else
{
lean_object* x_9; uint8_t x_10; uint8_t x_11; uint8_t x_12; uint8_t x_13; uint8_t x_14; uint8_t x_15; lean_object* x_16; lean_object* x_17;
lean_object* x_9; uint8_t x_10; uint8_t x_11; uint8_t x_12; uint8_t x_13; uint8_t x_14; uint8_t x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18;
x_9 = lean_ctor_get(x_5, 0);
x_10 = lean_ctor_get_uint8(x_5, sizeof(void*)*1);
x_11 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 1);
x_12 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 2);
x_13 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 3);
x_14 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 4);
x_15 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 5);
lean_inc(x_9);
lean_dec(x_5);
x_15 = 1;
x_16 = lean_alloc_ctor(0, 1, 6);
lean_ctor_set(x_16, 0, x_9);
lean_ctor_set_uint8(x_16, sizeof(void*)*1, x_10);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 1, x_11);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 2, x_12);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 3, x_13);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 4, x_14);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 5, x_15);
lean_ctor_set(x_2, 0, x_16);
x_17 = l_Lean_Meta_whnf(x_1, x_2, x_3);
return x_17;
x_16 = 1;
x_17 = lean_alloc_ctor(0, 1, 7);
lean_ctor_set(x_17, 0, x_9);
lean_ctor_set_uint8(x_17, sizeof(void*)*1, x_10);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 1, x_11);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 2, x_12);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 3, x_13);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 4, x_14);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 5, x_15);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 6, x_16);
lean_ctor_set(x_2, 0, x_17);
x_18 = l_Lean_Meta_whnf(x_1, x_2, x_3);
return x_18;
}
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; uint8_t x_23; uint8_t x_24; uint8_t x_25; uint8_t x_26; lean_object* x_27; uint8_t x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_18 = lean_ctor_get(x_2, 0);
x_19 = lean_ctor_get(x_2, 1);
x_20 = lean_ctor_get(x_2, 2);
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; uint8_t x_24; uint8_t x_25; uint8_t x_26; uint8_t x_27; uint8_t x_28; lean_object* x_29; uint8_t x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
x_19 = lean_ctor_get(x_2, 0);
x_20 = lean_ctor_get(x_2, 1);
x_21 = lean_ctor_get(x_2, 2);
lean_inc(x_21);
lean_inc(x_20);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_2);
x_21 = lean_ctor_get(x_18, 0);
lean_inc(x_21);
x_22 = lean_ctor_get_uint8(x_18, sizeof(void*)*1);
x_23 = lean_ctor_get_uint8(x_18, sizeof(void*)*1 + 1);
x_24 = lean_ctor_get_uint8(x_18, sizeof(void*)*1 + 2);
x_25 = lean_ctor_get_uint8(x_18, sizeof(void*)*1 + 3);
x_26 = lean_ctor_get_uint8(x_18, sizeof(void*)*1 + 4);
if (lean_is_exclusive(x_18)) {
lean_ctor_release(x_18, 0);
x_27 = x_18;
x_22 = lean_ctor_get(x_19, 0);
lean_inc(x_22);
x_23 = lean_ctor_get_uint8(x_19, sizeof(void*)*1);
x_24 = lean_ctor_get_uint8(x_19, sizeof(void*)*1 + 1);
x_25 = lean_ctor_get_uint8(x_19, sizeof(void*)*1 + 2);
x_26 = lean_ctor_get_uint8(x_19, sizeof(void*)*1 + 3);
x_27 = lean_ctor_get_uint8(x_19, sizeof(void*)*1 + 4);
x_28 = lean_ctor_get_uint8(x_19, sizeof(void*)*1 + 5);
if (lean_is_exclusive(x_19)) {
lean_ctor_release(x_19, 0);
x_29 = x_19;
} else {
lean_dec_ref(x_18);
x_27 = lean_box(0);
lean_dec_ref(x_19);
x_29 = lean_box(0);
}
x_28 = 1;
if (lean_is_scalar(x_27)) {
x_29 = lean_alloc_ctor(0, 1, 6);
x_30 = 1;
if (lean_is_scalar(x_29)) {
x_31 = lean_alloc_ctor(0, 1, 7);
} else {
x_29 = x_27;
x_31 = x_29;
}
lean_ctor_set(x_29, 0, x_21);
lean_ctor_set_uint8(x_29, sizeof(void*)*1, x_22);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 1, x_23);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 2, x_24);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 3, x_25);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 4, x_26);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 5, x_28);
x_30 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_30, 0, x_29);
lean_ctor_set(x_30, 1, x_19);
lean_ctor_set(x_30, 2, x_20);
x_31 = l_Lean_Meta_whnf(x_1, x_30, x_3);
return x_31;
lean_ctor_set(x_31, 0, x_22);
lean_ctor_set_uint8(x_31, sizeof(void*)*1, x_23);
lean_ctor_set_uint8(x_31, sizeof(void*)*1 + 1, x_24);
lean_ctor_set_uint8(x_31, sizeof(void*)*1 + 2, x_25);
lean_ctor_set_uint8(x_31, sizeof(void*)*1 + 3, x_26);
lean_ctor_set_uint8(x_31, sizeof(void*)*1 + 4, x_27);
lean_ctor_set_uint8(x_31, sizeof(void*)*1 + 5, x_28);
lean_ctor_set_uint8(x_31, sizeof(void*)*1 + 6, x_30);
x_32 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_32, 0, x_31);
lean_ctor_set(x_32, 1, x_20);
lean_ctor_set(x_32, 2, x_21);
x_33 = l_Lean_Meta_whnf(x_1, x_32, x_3);
return x_33;
}
}
}
lean_object* l_Lean_Meta_whnfD(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Meta_whnfUsingDefault(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_Meta_approxDefEq___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -40703,6 +40756,7 @@ x_7 = 1;
lean_ctor_set_uint8(x_5, sizeof(void*)*1, x_7);
lean_ctor_set_uint8(x_5, sizeof(void*)*1 + 1, x_7);
lean_ctor_set_uint8(x_5, sizeof(void*)*1 + 2, x_7);
lean_ctor_set_uint8(x_5, sizeof(void*)*1 + 3, x_7);
x_8 = lean_apply_2(x_1, x_2, x_3);
return x_8;
}
@ -40710,20 +40764,21 @@ else
{
lean_object* x_9; uint8_t x_10; uint8_t x_11; uint8_t x_12; uint8_t x_13; lean_object* x_14; lean_object* x_15;
x_9 = lean_ctor_get(x_5, 0);
x_10 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 3);
x_11 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 4);
x_12 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 5);
x_10 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 4);
x_11 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 5);
x_12 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 6);
lean_inc(x_9);
lean_dec(x_5);
x_13 = 1;
x_14 = lean_alloc_ctor(0, 1, 6);
x_14 = lean_alloc_ctor(0, 1, 7);
lean_ctor_set(x_14, 0, x_9);
lean_ctor_set_uint8(x_14, sizeof(void*)*1, x_13);
lean_ctor_set_uint8(x_14, sizeof(void*)*1 + 1, x_13);
lean_ctor_set_uint8(x_14, sizeof(void*)*1 + 2, x_13);
lean_ctor_set_uint8(x_14, sizeof(void*)*1 + 3, x_10);
lean_ctor_set_uint8(x_14, sizeof(void*)*1 + 4, x_11);
lean_ctor_set_uint8(x_14, sizeof(void*)*1 + 5, x_12);
lean_ctor_set_uint8(x_14, sizeof(void*)*1 + 3, x_13);
lean_ctor_set_uint8(x_14, sizeof(void*)*1 + 4, x_10);
lean_ctor_set_uint8(x_14, sizeof(void*)*1 + 5, x_11);
lean_ctor_set_uint8(x_14, sizeof(void*)*1 + 6, x_12);
lean_ctor_set(x_2, 0, x_14);
x_15 = lean_apply_2(x_1, x_2, x_3);
return x_15;
@ -40741,9 +40796,9 @@ lean_inc(x_16);
lean_dec(x_2);
x_19 = lean_ctor_get(x_16, 0);
lean_inc(x_19);
x_20 = lean_ctor_get_uint8(x_16, sizeof(void*)*1 + 3);
x_21 = lean_ctor_get_uint8(x_16, sizeof(void*)*1 + 4);
x_22 = lean_ctor_get_uint8(x_16, sizeof(void*)*1 + 5);
x_20 = lean_ctor_get_uint8(x_16, sizeof(void*)*1 + 4);
x_21 = lean_ctor_get_uint8(x_16, sizeof(void*)*1 + 5);
x_22 = lean_ctor_get_uint8(x_16, sizeof(void*)*1 + 6);
if (lean_is_exclusive(x_16)) {
lean_ctor_release(x_16, 0);
x_23 = x_16;
@ -40753,7 +40808,7 @@ if (lean_is_exclusive(x_16)) {
}
x_24 = 1;
if (lean_is_scalar(x_23)) {
x_25 = lean_alloc_ctor(0, 1, 6);
x_25 = lean_alloc_ctor(0, 1, 7);
} else {
x_25 = x_23;
}
@ -40761,9 +40816,10 @@ lean_ctor_set(x_25, 0, x_19);
lean_ctor_set_uint8(x_25, sizeof(void*)*1, x_24);
lean_ctor_set_uint8(x_25, sizeof(void*)*1 + 1, x_24);
lean_ctor_set_uint8(x_25, sizeof(void*)*1 + 2, x_24);
lean_ctor_set_uint8(x_25, sizeof(void*)*1 + 3, x_20);
lean_ctor_set_uint8(x_25, sizeof(void*)*1 + 4, x_21);
lean_ctor_set_uint8(x_25, sizeof(void*)*1 + 5, x_22);
lean_ctor_set_uint8(x_25, sizeof(void*)*1 + 3, x_24);
lean_ctor_set_uint8(x_25, sizeof(void*)*1 + 4, x_20);
lean_ctor_set_uint8(x_25, sizeof(void*)*1 + 5, x_21);
lean_ctor_set_uint8(x_25, sizeof(void*)*1 + 6, x_22);
x_26 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_17);
@ -45877,14 +45933,15 @@ uint8_t x_6; uint8_t x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_6 = 0;
x_7 = 1;
lean_inc(x_3);
x_8 = lean_alloc_ctor(0, 1, 6);
x_8 = lean_alloc_ctor(0, 1, 7);
lean_ctor_set(x_8, 0, x_3);
lean_ctor_set_uint8(x_8, sizeof(void*)*1, x_6);
lean_ctor_set_uint8(x_8, sizeof(void*)*1 + 1, x_6);
lean_ctor_set_uint8(x_8, sizeof(void*)*1 + 2, x_6);
lean_ctor_set_uint8(x_8, sizeof(void*)*1 + 3, x_6);
lean_ctor_set_uint8(x_8, sizeof(void*)*1 + 4, x_6);
lean_ctor_set_uint8(x_8, sizeof(void*)*1 + 5, x_7);
lean_ctor_set_uint8(x_8, sizeof(void*)*1 + 5, x_6);
lean_ctor_set_uint8(x_8, sizeof(void*)*1 + 6, x_7);
x_9 = l_Lean_LocalContext_Inhabited___closed__2;
x_10 = l_Array_empty___closed__1;
x_11 = lean_alloc_ctor(0, 3, 0);

1702
stage0/stdlib/Init/Lean/Meta/Check.c
View file

File diff suppressed because it is too large Load diff

894
stage0/stdlib/Init/Lean/Meta/DiscrTree.c
View file

File diff suppressed because it is too large Load diff

16308
stage0/stdlib/Init/Lean/Meta/ExprDefEq.c
View file

File diff suppressed because it is too large Load diff

296
stage0/stdlib/Init/Lean/Meta/FunInfo.c
View file

@ -1552,7 +1552,7 @@ _start:
lean_object* x_6; uint8_t x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_6 = lean_ctor_get(x_4, 0);
lean_inc(x_6);
x_7 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 5);
x_7 = lean_ctor_get_uint8(x_6, sizeof(void*)*1 + 6);
lean_dec(x_6);
x_8 = lean_ctor_get(x_5, 2);
lean_inc(x_8);
@ -9516,7 +9516,7 @@ if (x_8 == 0)
{
lean_object* x_9; uint8_t x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_9 = lean_ctor_get(x_5, 0);
x_10 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 5);
x_10 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 6);
x_11 = lean_ctor_get(x_4, 2);
lean_inc(x_11);
x_12 = lean_ctor_get(x_11, 1);
@ -9554,7 +9554,7 @@ x_21 = lean_ctor_get(x_15, 1);
lean_inc(x_21);
lean_dec(x_15);
x_22 = 1;
lean_ctor_set_uint8(x_5, sizeof(void*)*1 + 5, x_22);
lean_ctor_set_uint8(x_5, sizeof(void*)*1 + 6, x_22);
x_23 = l___private_Init_Lean_Meta_Basic_6__forallTelescopeReducingAux___at___private_Init_Lean_Meta_FunInfo_6__getFunInfoAux___spec__2(x_20, x_2, x_3, x_21);
if (lean_obj_tag(x_23) == 0)
{
@ -9792,7 +9792,7 @@ x_75 = lean_ctor_get(x_15, 1);
lean_inc(x_75);
lean_dec(x_15);
x_76 = 1;
lean_ctor_set_uint8(x_5, sizeof(void*)*1 + 5, x_76);
lean_ctor_set_uint8(x_5, sizeof(void*)*1 + 6, x_76);
x_77 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_77, 0, x_5);
lean_ctor_set(x_77, 1, x_6);
@ -9962,7 +9962,7 @@ return x_106;
}
else
{
lean_object* x_107; uint8_t x_108; uint8_t x_109; uint8_t x_110; uint8_t x_111; uint8_t x_112; uint8_t x_113; lean_object* x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117;
lean_object* x_107; uint8_t x_108; uint8_t x_109; uint8_t x_110; uint8_t x_111; uint8_t x_112; uint8_t x_113; uint8_t x_114; lean_object* x_115; lean_object* x_116; lean_object* x_117; lean_object* x_118;
x_107 = lean_ctor_get(x_5, 0);
x_108 = lean_ctor_get_uint8(x_5, sizeof(void*)*1);
x_109 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 1);
@ -9970,219 +9970,221 @@ x_110 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 2);
x_111 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 3);
x_112 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 4);
x_113 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 5);
x_114 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 6);
lean_inc(x_107);
lean_dec(x_5);
x_114 = lean_ctor_get(x_4, 2);
lean_inc(x_114);
x_115 = lean_ctor_get(x_114, 1);
x_115 = lean_ctor_get(x_4, 2);
lean_inc(x_115);
lean_dec(x_114);
x_116 = lean_ctor_get(x_115, 1);
lean_inc(x_116);
lean_dec(x_115);
lean_inc(x_2);
lean_inc(x_1);
x_116 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_116, 0, x_1);
lean_ctor_set(x_116, 1, x_2);
lean_ctor_set_uint8(x_116, sizeof(void*)*2, x_113);
x_117 = l_PersistentHashMap_find___at___private_Init_Lean_Meta_FunInfo_1__checkFunInfoCache___spec__1(x_115, x_116);
lean_dec(x_115);
if (lean_obj_tag(x_117) == 0)
x_117 = lean_alloc_ctor(0, 2, 1);
lean_ctor_set(x_117, 0, x_1);
lean_ctor_set(x_117, 1, x_2);
lean_ctor_set_uint8(x_117, sizeof(void*)*2, x_114);
x_118 = l_PersistentHashMap_find___at___private_Init_Lean_Meta_FunInfo_1__checkFunInfoCache___spec__1(x_116, x_117);
lean_dec(x_116);
if (lean_obj_tag(x_118) == 0)
{
lean_object* x_118; lean_object* x_119;
lean_object* x_119; lean_object* x_120;
lean_inc(x_3);
x_118 = l_Lean_Meta_inferType(x_1, x_3, x_4);
x_119 = l_Lean_Meta_inferType(x_1, x_3, x_4);
if (lean_is_exclusive(x_3)) {
lean_ctor_release(x_3, 0);
lean_ctor_release(x_3, 1);
lean_ctor_release(x_3, 2);
x_119 = x_3;
x_120 = x_3;
} else {
lean_dec_ref(x_3);
x_119 = lean_box(0);
x_120 = lean_box(0);
}
if (lean_obj_tag(x_118) == 0)
if (lean_obj_tag(x_119) == 0)
{
lean_object* x_120; lean_object* x_121; uint8_t x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125;
x_120 = lean_ctor_get(x_118, 0);
lean_inc(x_120);
x_121 = lean_ctor_get(x_118, 1);
lean_object* x_121; lean_object* x_122; uint8_t x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126;
x_121 = lean_ctor_get(x_119, 0);
lean_inc(x_121);
lean_dec(x_118);
x_122 = 1;
x_123 = lean_alloc_ctor(0, 1, 6);
lean_ctor_set(x_123, 0, x_107);
lean_ctor_set_uint8(x_123, sizeof(void*)*1, x_108);
lean_ctor_set_uint8(x_123, sizeof(void*)*1 + 1, x_109);
lean_ctor_set_uint8(x_123, sizeof(void*)*1 + 2, x_110);
lean_ctor_set_uint8(x_123, sizeof(void*)*1 + 3, x_111);
lean_ctor_set_uint8(x_123, sizeof(void*)*1 + 4, x_112);
lean_ctor_set_uint8(x_123, sizeof(void*)*1 + 5, x_122);
if (lean_is_scalar(x_119)) {
x_124 = lean_alloc_ctor(0, 3, 0);
x_122 = lean_ctor_get(x_119, 1);
lean_inc(x_122);
lean_dec(x_119);
x_123 = 1;
x_124 = lean_alloc_ctor(0, 1, 7);
lean_ctor_set(x_124, 0, x_107);
lean_ctor_set_uint8(x_124, sizeof(void*)*1, x_108);
lean_ctor_set_uint8(x_124, sizeof(void*)*1 + 1, x_109);
lean_ctor_set_uint8(x_124, sizeof(void*)*1 + 2, x_110);
lean_ctor_set_uint8(x_124, sizeof(void*)*1 + 3, x_111);
lean_ctor_set_uint8(x_124, sizeof(void*)*1 + 4, x_112);
lean_ctor_set_uint8(x_124, sizeof(void*)*1 + 5, x_113);
lean_ctor_set_uint8(x_124, sizeof(void*)*1 + 6, x_123);
if (lean_is_scalar(x_120)) {
x_125 = lean_alloc_ctor(0, 3, 0);
} else {
x_124 = x_119;
x_125 = x_120;
}
lean_ctor_set(x_124, 0, x_123);
lean_ctor_set(x_124, 1, x_6);
lean_ctor_set(x_124, 2, x_7);
x_125 = l___private_Init_Lean_Meta_Basic_6__forallTelescopeReducingAux___at___private_Init_Lean_Meta_FunInfo_6__getFunInfoAux___spec__2(x_120, x_2, x_124, x_121);
if (lean_obj_tag(x_125) == 0)
lean_ctor_set(x_125, 0, x_124);
lean_ctor_set(x_125, 1, x_6);
lean_ctor_set(x_125, 2, x_7);
x_126 = l___private_Init_Lean_Meta_Basic_6__forallTelescopeReducingAux___at___private_Init_Lean_Meta_FunInfo_6__getFunInfoAux___spec__2(x_121, x_2, x_125, x_122);
if (lean_obj_tag(x_126) == 0)
{
lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143;
x_126 = lean_ctor_get(x_125, 1);
lean_inc(x_126);
x_127 = lean_ctor_get(x_126, 2);
lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134; lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; lean_object* x_141; lean_object* x_142; lean_object* x_143; lean_object* x_144;
x_127 = lean_ctor_get(x_126, 1);
lean_inc(x_127);
x_128 = lean_ctor_get(x_125, 0);
x_128 = lean_ctor_get(x_127, 2);
lean_inc(x_128);
if (lean_is_exclusive(x_125)) {
lean_ctor_release(x_125, 0);
lean_ctor_release(x_125, 1);
x_129 = x_125;
} else {
lean_dec_ref(x_125);
x_129 = lean_box(0);
}
x_130 = lean_ctor_get(x_126, 0);
lean_inc(x_130);
x_131 = lean_ctor_get(x_126, 1);
lean_inc(x_131);
x_132 = lean_ctor_get(x_126, 3);
lean_inc(x_132);
x_133 = lean_ctor_get(x_126, 4);
lean_inc(x_133);
x_134 = lean_ctor_get(x_126, 5);
lean_inc(x_134);
x_129 = lean_ctor_get(x_126, 0);
lean_inc(x_129);
if (lean_is_exclusive(x_126)) {
lean_ctor_release(x_126, 0);
lean_ctor_release(x_126, 1);
lean_ctor_release(x_126, 2);
lean_ctor_release(x_126, 3);
lean_ctor_release(x_126, 4);
lean_ctor_release(x_126, 5);
x_135 = x_126;
x_130 = x_126;
} else {
lean_dec_ref(x_126);
x_135 = lean_box(0);
x_130 = lean_box(0);
}
x_136 = lean_ctor_get(x_127, 0);
lean_inc(x_136);
x_137 = lean_ctor_get(x_127, 1);
lean_inc(x_137);
x_138 = lean_ctor_get(x_127, 2);
lean_inc(x_138);
x_131 = lean_ctor_get(x_127, 0);
lean_inc(x_131);
x_132 = lean_ctor_get(x_127, 1);
lean_inc(x_132);
x_133 = lean_ctor_get(x_127, 3);
lean_inc(x_133);
x_134 = lean_ctor_get(x_127, 4);
lean_inc(x_134);
x_135 = lean_ctor_get(x_127, 5);
lean_inc(x_135);
if (lean_is_exclusive(x_127)) {
lean_ctor_release(x_127, 0);
lean_ctor_release(x_127, 1);
lean_ctor_release(x_127, 2);
x_139 = x_127;
lean_ctor_release(x_127, 3);
lean_ctor_release(x_127, 4);
lean_ctor_release(x_127, 5);
x_136 = x_127;
} else {
lean_dec_ref(x_127);
x_139 = lean_box(0);
x_136 = lean_box(0);
}
lean_inc(x_128);
x_140 = l_PersistentHashMap_insert___at___private_Init_Lean_Meta_FunInfo_1__checkFunInfoCache___spec__4(x_137, x_116, x_128);
if (lean_is_scalar(x_139)) {
x_141 = lean_alloc_ctor(0, 3, 0);
x_137 = lean_ctor_get(x_128, 0);
lean_inc(x_137);
x_138 = lean_ctor_get(x_128, 1);
lean_inc(x_138);
x_139 = lean_ctor_get(x_128, 2);
lean_inc(x_139);
if (lean_is_exclusive(x_128)) {
lean_ctor_release(x_128, 0);
lean_ctor_release(x_128, 1);
lean_ctor_release(x_128, 2);
x_140 = x_128;
} else {
x_141 = x_139;
lean_dec_ref(x_128);
x_140 = lean_box(0);
}
lean_ctor_set(x_141, 0, x_136);
lean_ctor_set(x_141, 1, x_140);
lean_ctor_set(x_141, 2, x_138);
if (lean_is_scalar(x_135)) {
x_142 = lean_alloc_ctor(0, 6, 0);
lean_inc(x_129);
x_141 = l_PersistentHashMap_insert___at___private_Init_Lean_Meta_FunInfo_1__checkFunInfoCache___spec__4(x_138, x_117, x_129);
if (lean_is_scalar(x_140)) {
x_142 = lean_alloc_ctor(0, 3, 0);
} else {
x_142 = x_135;
x_142 = x_140;
}
lean_ctor_set(x_142, 0, x_130);
lean_ctor_set(x_142, 1, x_131);
lean_ctor_set(x_142, 2, x_141);
lean_ctor_set(x_142, 3, x_132);
lean_ctor_set(x_142, 4, x_133);
lean_ctor_set(x_142, 5, x_134);
if (lean_is_scalar(x_129)) {
x_143 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_142, 0, x_137);
lean_ctor_set(x_142, 1, x_141);
lean_ctor_set(x_142, 2, x_139);
if (lean_is_scalar(x_136)) {
x_143 = lean_alloc_ctor(0, 6, 0);
} else {
x_143 = x_129;
x_143 = x_136;
}
lean_ctor_set(x_143, 0, x_128);
lean_ctor_set(x_143, 1, x_142);
return x_143;
lean_ctor_set(x_143, 0, x_131);
lean_ctor_set(x_143, 1, x_132);
lean_ctor_set(x_143, 2, x_142);
lean_ctor_set(x_143, 3, x_133);
lean_ctor_set(x_143, 4, x_134);
lean_ctor_set(x_143, 5, x_135);
if (lean_is_scalar(x_130)) {
x_144 = lean_alloc_ctor(0, 2, 0);
} else {
x_144 = x_130;
}
lean_ctor_set(x_144, 0, x_129);
lean_ctor_set(x_144, 1, x_143);
return x_144;
}
else
{
lean_object* x_144; lean_object* x_145; lean_object* x_146; lean_object* x_147;
lean_dec(x_116);
x_144 = lean_ctor_get(x_125, 0);
lean_inc(x_144);
x_145 = lean_ctor_get(x_125, 1);
lean_object* x_145; lean_object* x_146; lean_object* x_147; lean_object* x_148;
lean_dec(x_117);
x_145 = lean_ctor_get(x_126, 0);
lean_inc(x_145);
if (lean_is_exclusive(x_125)) {
lean_ctor_release(x_125, 0);
lean_ctor_release(x_125, 1);
x_146 = x_125;
x_146 = lean_ctor_get(x_126, 1);
lean_inc(x_146);
if (lean_is_exclusive(x_126)) {
lean_ctor_release(x_126, 0);
lean_ctor_release(x_126, 1);
x_147 = x_126;
} else {
lean_dec_ref(x_125);
x_146 = lean_box(0);
lean_dec_ref(x_126);
x_147 = lean_box(0);
}
if (lean_is_scalar(x_146)) {
x_147 = lean_alloc_ctor(1, 2, 0);
if (lean_is_scalar(x_147)) {
x_148 = lean_alloc_ctor(1, 2, 0);
} else {
x_147 = x_146;
x_148 = x_147;
}
lean_ctor_set(x_147, 0, x_144);
lean_ctor_set(x_147, 1, x_145);
return x_147;
lean_ctor_set(x_148, 0, x_145);
lean_ctor_set(x_148, 1, x_146);
return x_148;
}
}
else
{
lean_object* x_148; lean_object* x_149; lean_object* x_150; lean_object* x_151;
lean_dec(x_119);
lean_dec(x_116);
lean_object* x_149; lean_object* x_150; lean_object* x_151; lean_object* x_152;
lean_dec(x_120);
lean_dec(x_117);
lean_dec(x_107);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_2);
x_148 = lean_ctor_get(x_118, 0);
lean_inc(x_148);
x_149 = lean_ctor_get(x_118, 1);
x_149 = lean_ctor_get(x_119, 0);
lean_inc(x_149);
if (lean_is_exclusive(x_118)) {
lean_ctor_release(x_118, 0);
lean_ctor_release(x_118, 1);
x_150 = x_118;
x_150 = lean_ctor_get(x_119, 1);
lean_inc(x_150);
if (lean_is_exclusive(x_119)) {
lean_ctor_release(x_119, 0);
lean_ctor_release(x_119, 1);
x_151 = x_119;
} else {
lean_dec_ref(x_118);
x_150 = lean_box(0);
lean_dec_ref(x_119);
x_151 = lean_box(0);
}
if (lean_is_scalar(x_150)) {
x_151 = lean_alloc_ctor(1, 2, 0);
if (lean_is_scalar(x_151)) {
x_152 = lean_alloc_ctor(1, 2, 0);
} else {
x_151 = x_150;
x_152 = x_151;
}
lean_ctor_set(x_151, 0, x_148);
lean_ctor_set(x_151, 1, x_149);
return x_151;
lean_ctor_set(x_152, 0, x_149);
lean_ctor_set(x_152, 1, x_150);
return x_152;
}
}
else
{
lean_object* x_152; lean_object* x_153;
lean_dec(x_116);
lean_object* x_153; lean_object* x_154;
lean_dec(x_117);
lean_dec(x_107);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_152 = lean_ctor_get(x_117, 0);
lean_inc(x_152);
lean_dec(x_117);
x_153 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_153, 0, x_152);
lean_ctor_set(x_153, 1, x_4);
return x_153;
x_153 = lean_ctor_get(x_118, 0);
lean_inc(x_153);
lean_dec(x_118);
x_154 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_154, 0, x_153);
lean_ctor_set(x_154, 1, x_4);
return x_154;
}
}
}

108
stage0/stdlib/Init/Lean/Meta/InferType.c
View file

@ -109,7 +109,6 @@ lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Meta_InferType_
lean_object* l_Lean_mkLevelSucc(lean_object*);
uint8_t lean_expr_equal(lean_object*, lean_object*);
uint8_t l_USize_decLe(size_t, size_t);
lean_object* l_Lean_Meta_whnfUsingDefault(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_foldMAux___main___at___private_Init_Lean_Meta_InferType_1__inferAppType___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Bool_toLBool(uint8_t);
lean_object* l___private_Init_Lean_Meta_InferType_6__withLocalDecl___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -132,6 +131,7 @@ lean_object* l___private_Init_Lean_Meta_InferType_4__inferForallType(lean_object
lean_object* l___private_Init_Lean_Meta_InferType_6__withLocalDecl(lean_object*);
lean_object* l___private_Init_Lean_Meta_InferType_6__withLocalDecl___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_InferType_17__isTypeQuickApp___main(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_whnfD(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at___private_Init_Lean_Meta_InferType_4__inferForallType___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_InferType_7__inferMVarType___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_InferType_17__isTypeQuickApp(lean_object*, lean_object*, lean_object*, lean_object*);
@ -1722,7 +1722,7 @@ x_6 = lean_ctor_get(x_4, 1);
lean_inc(x_6);
lean_dec(x_4);
lean_inc(x_2);
x_7 = l_Lean_Meta_whnfUsingDefault(x_5, x_2, x_6);
x_7 = l_Lean_Meta_whnfD(x_5, x_2, x_6);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8;
@ -4705,78 +4705,82 @@ if (x_6 == 0)
{
uint8_t x_7; lean_object* x_8;
x_7 = 1;
lean_ctor_set_uint8(x_5, sizeof(void*)*1 + 5, x_7);
lean_ctor_set_uint8(x_5, sizeof(void*)*1 + 6, x_7);
x_8 = l___private_Init_Lean_Meta_InferType_10__inferTypeAux___main(x_1, x_2, x_3);
return x_8;
}
else
{
lean_object* x_9; uint8_t x_10; uint8_t x_11; uint8_t x_12; uint8_t x_13; uint8_t x_14; uint8_t x_15; lean_object* x_16; lean_object* x_17;
lean_object* x_9; uint8_t x_10; uint8_t x_11; uint8_t x_12; uint8_t x_13; uint8_t x_14; uint8_t x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18;
x_9 = lean_ctor_get(x_5, 0);
x_10 = lean_ctor_get_uint8(x_5, sizeof(void*)*1);
x_11 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 1);
x_12 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 2);
x_13 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 3);
x_14 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 4);
x_15 = lean_ctor_get_uint8(x_5, sizeof(void*)*1 + 5);
lean_inc(x_9);
lean_dec(x_5);
x_15 = 1;
x_16 = lean_alloc_ctor(0, 1, 6);
lean_ctor_set(x_16, 0, x_9);
lean_ctor_set_uint8(x_16, sizeof(void*)*1, x_10);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 1, x_11);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 2, x_12);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 3, x_13);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 4, x_14);
lean_ctor_set_uint8(x_16, sizeof(void*)*1 + 5, x_15);
lean_ctor_set(x_2, 0, x_16);
x_17 = l___private_Init_Lean_Meta_InferType_10__inferTypeAux___main(x_1, x_2, x_3);
return x_17;
x_16 = 1;
x_17 = lean_alloc_ctor(0, 1, 7);
lean_ctor_set(x_17, 0, x_9);
lean_ctor_set_uint8(x_17, sizeof(void*)*1, x_10);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 1, x_11);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 2, x_12);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 3, x_13);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 4, x_14);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 5, x_15);
lean_ctor_set_uint8(x_17, sizeof(void*)*1 + 6, x_16);
lean_ctor_set(x_2, 0, x_17);
x_18 = l___private_Init_Lean_Meta_InferType_10__inferTypeAux___main(x_1, x_2, x_3);
return x_18;
}
}
else
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; uint8_t x_23; uint8_t x_24; uint8_t x_25; uint8_t x_26; lean_object* x_27; uint8_t x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_18 = lean_ctor_get(x_2, 0);
x_19 = lean_ctor_get(x_2, 1);
x_20 = lean_ctor_get(x_2, 2);
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; uint8_t x_24; uint8_t x_25; uint8_t x_26; uint8_t x_27; uint8_t x_28; lean_object* x_29; uint8_t x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
x_19 = lean_ctor_get(x_2, 0);
x_20 = lean_ctor_get(x_2, 1);
x_21 = lean_ctor_get(x_2, 2);
lean_inc(x_21);
lean_inc(x_20);
lean_inc(x_19);
lean_inc(x_18);
lean_dec(x_2);
x_21 = lean_ctor_get(x_18, 0);
lean_inc(x_21);
x_22 = lean_ctor_get_uint8(x_18, sizeof(void*)*1);
x_23 = lean_ctor_get_uint8(x_18, sizeof(void*)*1 + 1);
x_24 = lean_ctor_get_uint8(x_18, sizeof(void*)*1 + 2);
x_25 = lean_ctor_get_uint8(x_18, sizeof(void*)*1 + 3);
x_26 = lean_ctor_get_uint8(x_18, sizeof(void*)*1 + 4);
if (lean_is_exclusive(x_18)) {
lean_ctor_release(x_18, 0);
x_27 = x_18;
x_22 = lean_ctor_get(x_19, 0);
lean_inc(x_22);
x_23 = lean_ctor_get_uint8(x_19, sizeof(void*)*1);
x_24 = lean_ctor_get_uint8(x_19, sizeof(void*)*1 + 1);
x_25 = lean_ctor_get_uint8(x_19, sizeof(void*)*1 + 2);
x_26 = lean_ctor_get_uint8(x_19, sizeof(void*)*1 + 3);
x_27 = lean_ctor_get_uint8(x_19, sizeof(void*)*1 + 4);
x_28 = lean_ctor_get_uint8(x_19, sizeof(void*)*1 + 5);
if (lean_is_exclusive(x_19)) {
lean_ctor_release(x_19, 0);
x_29 = x_19;
} else {
lean_dec_ref(x_18);
x_27 = lean_box(0);
lean_dec_ref(x_19);
x_29 = lean_box(0);
}
x_28 = 1;
if (lean_is_scalar(x_27)) {
x_29 = lean_alloc_ctor(0, 1, 6);
x_30 = 1;
if (lean_is_scalar(x_29)) {
x_31 = lean_alloc_ctor(0, 1, 7);
} else {
x_29 = x_27;
x_31 = x_29;
}
lean_ctor_set(x_29, 0, x_21);
lean_ctor_set_uint8(x_29, sizeof(void*)*1, x_22);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 1, x_23);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 2, x_24);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 3, x_25);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 4, x_26);
lean_ctor_set_uint8(x_29, sizeof(void*)*1 + 5, x_28);
x_30 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_30, 0, x_29);
lean_ctor_set(x_30, 1, x_19);
lean_ctor_set(x_30, 2, x_20);
x_31 = l___private_Init_Lean_Meta_InferType_10__inferTypeAux___main(x_1, x_30, x_3);
return x_31;
lean_ctor_set(x_31, 0, x_22);
lean_ctor_set_uint8(x_31, sizeof(void*)*1, x_23);
lean_ctor_set_uint8(x_31, sizeof(void*)*1 + 1, x_24);
lean_ctor_set_uint8(x_31, sizeof(void*)*1 + 2, x_25);
lean_ctor_set_uint8(x_31, sizeof(void*)*1 + 3, x_26);
lean_ctor_set_uint8(x_31, sizeof(void*)*1 + 4, x_27);
lean_ctor_set_uint8(x_31, sizeof(void*)*1 + 5, x_28);
lean_ctor_set_uint8(x_31, sizeof(void*)*1 + 6, x_30);
x_32 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_32, 0, x_31);
lean_ctor_set(x_32, 1, x_20);
lean_ctor_set(x_32, 2, x_21);
x_33 = l___private_Init_Lean_Meta_InferType_10__inferTypeAux___main(x_1, x_32, x_3);
return x_33;
}
}
}
@ -5569,7 +5573,7 @@ x_26 = lean_ctor_get(x_24, 1);
lean_inc(x_26);
lean_dec(x_24);
lean_inc(x_2);
x_27 = l_Lean_Meta_whnfUsingDefault(x_25, x_2, x_26);
x_27 = l_Lean_Meta_whnfD(x_25, x_2, x_26);
if (lean_obj_tag(x_27) == 0)
{
lean_object* x_28;
@ -7305,7 +7309,7 @@ lean_inc(x_25);
x_26 = lean_ctor_get(x_24, 1);
lean_inc(x_26);
lean_dec(x_24);
x_27 = l_Lean_Meta_whnfUsingDefault(x_25, x_2, x_26);
x_27 = l_Lean_Meta_whnfD(x_25, x_2, x_26);
if (lean_obj_tag(x_27) == 0)
{
lean_object* x_28;

5
stage0/stdlib/Init/Lean/Meta/Instances.c
View file

@ -3182,14 +3182,15 @@ lean_object* x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Lean_Options_empty;
x_2 = 0;
x_3 = 1;
x_4 = lean_alloc_ctor(0, 1, 6);
x_4 = lean_alloc_ctor(0, 1, 7);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, sizeof(void*)*1, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 1, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 2, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 3, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 4, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 5, x_3);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 5, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 6, x_3);
return x_4;
}
}

4
stage0/stdlib/Init/Lean/Meta/LevelDefEq.c
View file

@ -962,7 +962,7 @@ if (x_200 == 0)
{
lean_object* x_201; uint8_t x_202;
x_201 = lean_ctor_get(x_3, 0);
x_202 = lean_ctor_get_uint8(x_201, sizeof(void*)*1 + 3);
x_202 = lean_ctor_get_uint8(x_201, sizeof(void*)*1 + 4);
if (x_202 == 0)
{
uint8_t x_203; lean_object* x_204;
@ -1801,7 +1801,7 @@ if (x_328 == 0)
{
lean_object* x_329; uint8_t x_330;
x_329 = lean_ctor_get(x_3, 0);
x_330 = lean_ctor_get_uint8(x_329, sizeof(void*)*1 + 3);
x_330 = lean_ctor_get_uint8(x_329, sizeof(void*)*1 + 4);
if (x_330 == 0)
{
uint8_t x_331; lean_object* x_332; lean_object* x_333;

5
stage0/stdlib/Init/Lean/Meta/Message.c
View file

@ -193,14 +193,15 @@ lean_object* x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Lean_Options_empty;
x_2 = 0;
x_3 = 1;
x_4 = lean_alloc_ctor(0, 1, 6);
x_4 = lean_alloc_ctor(0, 1, 7);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, sizeof(void*)*1, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 1, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 2, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 3, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 4, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 5, x_3);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 5, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 6, x_3);
return x_4;
}
}

2935
stage0/stdlib/Init/Lean/Meta/SynthInstance.c
View file

File diff suppressed because it is too large Load diff