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 2021-07-27 14:19:53 -07:00
parent fb3ea8109f
commit 67f4d5bd57
54 changed files with 2715 additions and 1941 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
stage0/src/Init/System/IOError.lean generated
View file

@ -15,7 +15,7 @@ Imitate the structure of IOErrorType in Haskell:
https://hackage.haskell.org/package/base-4.12.0.0/docs/System-IO-Error.html#t:IOErrorType
-/
inductive IO.Error where
| alreadyExists (osCode : UInt32) (details : String) -- EEXIST, EINPROGRESS, EISCONN
| alreadyExists (filename : Option String) (osCode : UInt32) (details : String) -- EEXIST, EINPROGRESS, EISCONN
| otherError (osCode : UInt32) (details : String) -- EFAULT, default
| resourceBusy (osCode : UInt32) (details : String)
-- EADDRINUSE, EBUSY, EDEADLK, ETXTBSY
@ -61,6 +61,10 @@ instance : Coe String IO.Error := ⟨IO.userError⟩
namespace IO.Error
@[export lean_mk_io_error_already_exists_file]
def mkAlreadyExistsFile : String → UInt32 → String → IO.Error :=
alreadyExists ∘ some
@[export lean_mk_io_error_eof]
def mkEofError : Unit → IO.Error := fun _ =>
unexpectedEof
@ -103,7 +107,7 @@ def mkResourceExhausted : UInt32 → String → IO.Error :=
@[export lean_mk_io_error_already_exists]
def mkAlreadyExists : UInt32 → String → IO.Error :=
alreadyExists
alreadyExists none
@[export lean_mk_io_error_inappropriate_type]
def mkInappropriateType : UInt32 → String → IO.Error :=
@ -178,7 +182,8 @@ def toString : IO.Error → String
| permissionDenied none code details => otherErrorToString details code none
| resourceExhausted (some fn) code details => fopenErrorToString "resource exhausted" fn code details
| resourceExhausted none code details => otherErrorToString "resource exhausted" code details
| alreadyExists code details => otherErrorToString "already exists" code details
| alreadyExists none code details => otherErrorToString "already exists" code details
| alreadyExists (some fn) code details => fopenErrorToString "already exists" fn code details
| otherError code details => otherErrorToString details code none
| resourceBusy code details => otherErrorToString "resource busy" code details
| resourceVanished code details => otherErrorToString "resource vanished" code details

29
stage0/src/Lean/Elab/StructInst.lean generated
View file

@ -683,9 +683,10 @@ def mkDefaultValue? (struct : Struct) (cinfo : ConstantInfo) : TermElabM (Option
/-- If `e` is a projection function of one of the given structures, then reduce it -/
def reduceProjOf? (structNames : Array Name) (e : Expr) : MetaM (Option Expr) := do
if !e.isApp then pure none
if !e.isApp then
pure none
else match e.getAppFn with
| Expr.const name _ _ => do
| Expr.const name .. => do
let env ← getEnv
match env.getProjectionStructureName? name with
| some structName =>
@ -697,15 +698,17 @@ def reduceProjOf? (structNames : Array Name) (e : Expr) : MetaM (Option Expr) :=
| _ => pure none
/-- Reduce default value. It performs beta reduction and projections of the given structures. -/
partial def reduce (structNames : Array Name) : Expr → MetaM Expr
| e@(Expr.lam _ _ _ _) => lambdaLetTelescope e fun xs b => do mkLambdaFVars xs (← reduce structNames b)
| e@(Expr.forallE _ _ _ _) => forallTelescope e fun xs b => do mkForallFVars xs (← reduce structNames b)
| e@(Expr.letE _ _ _ _ _) => lambdaLetTelescope e fun xs b => do mkLetFVars xs (← reduce structNames b)
| e@(Expr.proj _ i b _) => do
partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
-- trace[Elab.struct] "reduce {e}"
match e with
| Expr.lam .. => lambdaLetTelescope e fun xs b => do mkLambdaFVars xs (← reduce structNames b)
| Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← reduce structNames b)
| Expr.letE .. => lambdaLetTelescope e fun xs b => do mkLetFVars xs (← reduce structNames b)
| Expr.proj _ i b _ => do
match (← Meta.project? b i) with
| some r => reduce structNames r
| none => return e.updateProj! (← reduce structNames b)
| e@(Expr.app f _ _) => do
| Expr.app f .. => do
match (← reduceProjOf? structNames e) with
| some r => reduce structNames r
| none =>
@ -717,15 +720,15 @@ partial def reduce (structNames : Array Name) : Expr → MetaM Expr
else
let args ← e.getAppArgs.mapM (reduce structNames)
return (mkAppN f' args)
| e@(Expr.mdata _ b _) => do
| Expr.mdata _ b _ => do
let b ← reduce structNames b
if (defaultMissing? e).isSome && !b.isMVar then
return b
else
return e.updateMData! b
| e@(Expr.mvar mvarId _) => do
| Expr.mvar mvarId _ => do
match (← getExprMVarAssignment? mvarId) with
| some val => if val.isMVar then reduce structNames val else pure val
| some val => if val.isMVar then pure val else reduce structNames val
| none => return e
| e => return e
@ -765,7 +768,8 @@ partial def step (struct : Struct) : M Unit :=
| FieldVal.nested struct => step struct
| _ => match field.expr? with
| none => unreachable!
| some expr => match defaultMissing? expr with
| some expr =>
match defaultMissing? expr with
| some (Expr.mvar mvarId _) =>
unless (← isExprMVarAssigned mvarId) do
let ctx ← read
@ -777,6 +781,7 @@ partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : Struct) : M
match findDefaultMissing? (← getMCtx) struct with
| none => pure () -- Done
| some field =>
trace[Elab.struct] "propagate [{d}] [field := {field}]: {struct}"
if d > hierarchyDepth then
throwErrorAt field.ref "field '{getFieldName field}' is missing"
else withReader (fun ctx => { ctx with maxDistance := d }) do

62
stage0/src/Lean/Elab/Structure.lean generated
View file

@ -104,7 +104,7 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
let useDefault := do
let declName := structDeclName ++ defaultCtorName
addAuxDeclarationRanges declName structStx[2] structStx[2]
pure { ref := structStx, modifiers := {}, inferMod := false, name := defaultCtorName, declName := declName }
pure { ref := structStx, modifiers := {}, inferMod := false, name := defaultCtorName, declName }
if structStx[5].isNone then
useDefault
else
@ -126,7 +126,7 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc
let declName ← applyVisibility ctorModifiers.visibility declName
addDocString' declName ctorModifiers.docString?
addAuxDeclarationRanges declName ctor[1] ctor[1]
pure { ref := ctor, name := name, modifiers := ctorModifiers, inferMod := inferMod, declName := declName }
pure { ref := ctor, name, modifiers := ctorModifiers, inferMod, declName }
def checkValidFieldModifier (modifiers : Modifiers) : TermElabM Unit := do
if modifiers.isNoncomputable then
@ -192,15 +192,15 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
let declName ← applyVisibility fieldModifiers.visibility declName
addDocString' declName fieldModifiers.docString?
return views.push {
ref := ident,
modifiers := fieldModifiers,
binderInfo := binfo,
inferMod := inferMod,
declName := declName,
name := name,
binders := binders,
type? := type?,
value? := value?
ref := ident
modifiers := fieldModifiers
binderInfo := binfo
inferMod
declName
name
binders
type?
value?
}
private def validStructType (type : Expr) : Bool :=
@ -235,7 +235,7 @@ private partial def processSubfields (structDeclName : Name) (parentFVar : Expr)
/- The following `declName` is only used for creating the `_default` auxiliary declaration name when
its default value is overwritten in the structure. -/
let declName := structDeclName ++ subfieldName
let infos := infos.push { name := subfieldName, declName := declName, fvar := subfieldFVar, kind := StructFieldKind.fromParent }
let infos := infos.push { name := subfieldName, declName, fvar := subfieldFVar, kind := StructFieldKind.fromParent }
loop (i+1) infos
else
k infos
@ -353,7 +353,7 @@ private def removeUnused (scopeVars : Array Expr) (params : Array Expr) (fieldIn
private def withUsed {α} (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo) (k : Array Expr → TermElabM α)
: TermElabM α := do
let (lctx, localInsts, vars) ← removeUnused scopeVars params fieldInfos
withLCtx lctx localInsts $ k vars
withLCtx lctx localInsts <| k vars
private def levelMVarToParamFVar (fvar : Expr) : StateRefT Nat TermElabM Unit := do
let type ← inferType fvar
@ -399,7 +399,7 @@ private def updateResultingUniverse (fieldInfos : Array StructFieldInfo) (type :
private def collectLevelParamsInFVar (s : CollectLevelParams.State) (fvar : Expr) : TermElabM CollectLevelParams.State := do
let type ← inferType fvar
let type ← instantiateMVars type
pure $ collectLevelParams s type
return collectLevelParams s type
private def collectLevelParamsInFVars (fvars : Array Expr) (s : CollectLevelParams.State) : TermElabM CollectLevelParams.State :=
fvars.foldlM collectLevelParamsInFVar s
@ -409,8 +409,8 @@ private def collectLevelParamsInStructure (structType : Expr) (scopeVars : Array
let s := collectLevelParams {} structType
let s ← collectLevelParamsInFVars scopeVars s
let s ← collectLevelParamsInFVars params s
let s ← fieldInfos.foldlM (fun (s : CollectLevelParams.State) info => collectLevelParamsInFVar s info.fvar) s
pure s.params
let s ← fieldInfos.foldlM (init := s) fun s info => collectLevelParamsInFVar s info.fvar
return s.params
private def addCtorFields (fieldInfos : Array StructFieldInfo) : Nat → Expr → TermElabM Expr
| 0, type => pure type
@ -424,7 +424,7 @@ private def addCtorFields (fieldInfos : Array StructFieldInfo) : Nat → Expr
let val := decl.value
addCtorFields fieldInfos i (type.instantiate1 val)
| StructFieldKind.subobject =>
let n := mkInternalSubobjectFieldName $ decl.userName
let n := mkInternalSubobjectFieldName decl.userName
addCtorFields fieldInfos i (mkForall n decl.binderInfo decl.type type)
| StructFieldKind.newField =>
addCtorFields fieldInfos i (mkForall decl.userName decl.binderInfo decl.type type)
@ -436,7 +436,7 @@ private def mkCtor (view : StructView) (levelParams : List Name) (params : Array
let type ← mkForallFVars params type
let type ← instantiateMVars type
let type := type.inferImplicit params.size !view.ctor.inferMod
pure { name := view.ctor.declName, type := type }
pure { name := view.ctor.declName, type }
@[extern "lean_mk_projections"]
private constant mkProjections (env : Environment) (structName : Name) (projs : List ProjectionInfo) (isClass : Bool) : Except KernelException Environment
@ -482,7 +482,7 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
Term.synthesizeSyntheticMVarsNoPostponing
let u ← getResultUniverse type
let inferLevel ← shouldInferResultUniverse u
withUsed view.scopeVars view.params fieldInfos $ fun scopeVars => do
withUsed view.scopeVars view.params fieldInfos fun scopeVars => do
let numParams := scopeVars.size + numExplicitParams
let fieldInfos ← levelMVarToParam scopeVars view.params fieldInfos
let type ← withRef view.ref do
@ -567,18 +567,18 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
let params ← Term.addAutoBoundImplicits params
let allUserLevelNames ← Term.getLevelNames
elabStructureView {
ref := stx
modifiers := modifiers
scopeLevelNames := scopeLevelNames
allUserLevelNames := allUserLevelNames
declName := declName
isClass := isClass
scopeVars := scopeVars
params := params
parents := parents
type := type
ctor := ctor
fields := fields
ref := stx
modifiers
scopeLevelNames
allUserLevelNames
declName
isClass
scopeVars
params
parents
type
ctor
fields
}
unless isClass do
mkSizeOfInstances declName

4
stage0/src/Lean/Parser/Command.lean generated
View file

@ -49,10 +49,10 @@ def derivingClasses := sepBy1 (group (ident >> optional (" with " >> Term.struc
def optDeriving := leading_parser optional (atomic ("deriving " >> notSymbol "instance") >> derivingClasses)
def «inductive» := leading_parser "inductive " >> declId >> optDeclSig >> optional (symbol ":=" <|> "where") >> many ctor >> optDeriving
def classInductive := leading_parser atomic (group (symbol "class " >> "inductive ")) >> declId >> optDeclSig >> optional (symbol ":=" <|> "where") >> many ctor >> optDeriving
def structExplicitBinder := leading_parser atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
def structExplicitBinder := leading_parser atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional (Term.binderTactic <|> Term.binderDefault) >> ")"
def structImplicitBinder := leading_parser atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
def structInstBinder := leading_parser atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
def structSimpleBinder := leading_parser atomic (declModifiers true >> ident) >> optional inferMod >> optDeclSig >> optional Term.binderDefault
def structSimpleBinder := leading_parser atomic (declModifiers true >> ident) >> optional inferMod >> optDeclSig >> optional (Term.binderTactic <|> Term.binderDefault)
def structFields := leading_parser manyIndent (ppLine >> checkColGe >>(structExplicitBinder <|> structImplicitBinder <|> structInstBinder <|> structSimpleBinder))
def structCtor := leading_parser atomic (declModifiers true >> ident >> optional inferMod >> " :: ")
def structureTk := leading_parser "structure "

4
stage0/src/Leanpkg.lean generated
View file

@ -40,10 +40,10 @@ partial def withLockFile (x : IO α) : IO α := do
-- https://docs.microsoft.com/en-us/cpp/c-runtime-library/reference/fopen-wfopen?view=msvc-160
-- ...? Let's use the slightly racy approach then.
if ← lockFileName.pathExists then
throw <| IO.Error.alreadyExists 0 ""
throw <| IO.Error.alreadyExists none 0 ""
discard <| IO.FS.Handle.mk lockFileName IO.FS.Mode.write
catch
| IO.Error.alreadyExists _ _ => do
| IO.Error.alreadyExists .. => do
if firstTime then
IO.eprintln s!"Waiting for prior leanpkg invocation to finish... (remove '{lockFileName}' if stuck)"
IO.sleep (ms := 300)

2
stage0/src/runtime/compact.cpp generated
View file

@ -272,8 +272,8 @@ void object_compactor::insert_mpz(object * o) {
size_t data_sz = sizeof(mp_limb_t) * nlimbs;
size_t sz = sizeof(mpz_object) + data_sz;
mpz_object * new_o = (mpz_object *)alloc(sz);
lean_set_non_heap_header((lean_object*)new_o, sz, LeanMPZ, 0);
memcpy(new_o, to_mpz(o), sizeof(mpz_object));
lean_set_non_heap_header((lean_object*)new_o, sz, LeanMPZ, 0);
__mpz_struct & m = new_o->m_value.m_val[0];
// we assume the limb array is the only indirection in an `__mpz_struct` and everything else can be bitcopied
void * data = reinterpret_cast<char*>(new_o) + sizeof(mpz_object);

9
stage0/src/runtime/io.cpp generated
View file

@ -52,6 +52,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
namespace lean {
extern "C" lean_object* lean_mk_io_error_already_exists(uint32_t, lean_object*);
extern "C" lean_object* lean_mk_io_error_already_exists_file(lean_object*, uint32_t, lean_object*);
extern "C" lean_object* lean_mk_io_error_eof(lean_object*);
extern "C" lean_object* lean_mk_io_error_hardware_fault(uint32_t, lean_object*);
extern "C" lean_object* lean_mk_io_error_illegal_operation(uint32_t, lean_object*);
@ -230,8 +231,12 @@ obj_res decode_io_error(int errnum, b_obj_arg fname) {
return lean_mk_io_error_no_such_thing_file(fname, errnum, details);
}
case EEXIST: case EINPROGRESS: case EISCONN:
lean_assert(fname == nullptr);
return lean_mk_io_error_already_exists(errnum, details);
if (fname == nullptr) {
return lean_mk_io_error_already_exists(errnum, details);
} else {
inc_ref(fname);
return lean_mk_io_error_already_exists_file(fname, errnum, details);
}
case EIO:
lean_assert(fname == nullptr);
return lean_mk_io_error_hardware_fault(errnum, details);

1754
stage0/stdlib/Init/System/IOError.c generated
View file

File diff suppressed because it is too large Load diff

16
stage0/stdlib/Lean/Attributes.c generated
View file

@ -3621,13 +3621,15 @@ return x_2;
static lean_object* _init_l_Lean_instInhabitedTagAttribute___lambda__1___closed__2() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_instInhabitedTagAttribute___lambda__1___closed__1;
x_2 = l_Lean_instInhabitedAttributeImplCore___closed__1;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_instInhabitedTagAttribute___lambda__1___closed__1;
x_3 = l_Lean_instInhabitedAttributeImplCore___closed__1;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_instInhabitedTagAttribute___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {

16
stage0/stdlib/Lean/AuxRecursor.c generated
View file

@ -264,13 +264,15 @@ return x_1;
static lean_object* _init_l_Lean_auxRecExt___elambda__4___rarg___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_auxRecExt___elambda__4___rarg___closed__1;
x_2 = l_Lean_auxRecExt___elambda__4___rarg___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_auxRecExt___elambda__4___rarg___closed__1;
x_3 = l_Lean_auxRecExt___elambda__4___rarg___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_auxRecExt___elambda__4___rarg(lean_object* x_1) {

16
stage0/stdlib/Lean/Class.c generated
View file

@ -2315,13 +2315,15 @@ return x_1;
static lean_object* _init_l_Lean_classExtension___elambda__4___rarg___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_classExtension___elambda__4___rarg___closed__1;
x_2 = l_Lean_classExtension___elambda__4___rarg___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_classExtension___elambda__4___rarg___closed__1;
x_3 = l_Lean_classExtension___elambda__4___rarg___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_classExtension___elambda__4___rarg(lean_object* x_1) {

16
stage0/stdlib/Lean/Compiler/ExportAttr.c generated
View file

@ -2268,13 +2268,15 @@ return x_1;
static lean_object* _init_l_Lean_exportAttr___lambda__3___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_exportAttr___lambda__3___closed__1;
x_2 = l_Lean_exportAttr___lambda__3___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_exportAttr___lambda__3___closed__1;
x_3 = l_Lean_exportAttr___lambda__3___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_exportAttr___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {

16
stage0/stdlib/Lean/Compiler/ExternAttr.c generated
View file

@ -2851,13 +2851,15 @@ return x_1;
static lean_object* _init_l_Lean_externAttr___lambda__3___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_externAttr___lambda__3___closed__1;
x_2 = l_Lean_externAttr___lambda__3___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_externAttr___lambda__3___closed__1;
x_3 = l_Lean_externAttr___lambda__3___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_externAttr___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {

16
stage0/stdlib/Lean/Compiler/IR/CompilerM.c generated
View file

@ -3099,13 +3099,15 @@ return x_2;
static lean_object* _init_l_Lean_IR_declMapExt___elambda__4___rarg___closed__2() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_IR_declMapExt___elambda__4___rarg___closed__1;
x_2 = l_Array_foldlMUnsafe_fold___at_Lean_IR_Log_format___spec__2___closed__1;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_IR_declMapExt___elambda__4___rarg___closed__1;
x_3 = l_Array_foldlMUnsafe_fold___at_Lean_IR_Log_format___spec__2___closed__1;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_IR_declMapExt___elambda__4___rarg(lean_object* x_1) {

16
stage0/stdlib/Lean/Compiler/IR/ElimDeadBranches.c generated
View file

@ -5227,13 +5227,15 @@ return x_1;
static lean_object* _init_l_Lean_IR_UnreachableBranches_functionSummariesExt___elambda__4___rarg___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_IR_UnreachableBranches_functionSummariesExt___elambda__4___rarg___closed__1;
x_2 = l_Lean_IR_UnreachableBranches_functionSummariesExt___elambda__4___rarg___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_IR_UnreachableBranches_functionSummariesExt___elambda__4___rarg___closed__1;
x_3 = l_Lean_IR_UnreachableBranches_functionSummariesExt___elambda__4___rarg___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_IR_UnreachableBranches_functionSummariesExt___elambda__4___rarg(lean_object* x_1) {

16
stage0/stdlib/Lean/Compiler/IR/UnboxResult.c generated
View file

@ -537,13 +537,15 @@ return x_1;
static lean_object* _init_l_Lean_IR_UnboxResult_unboxAttr___lambda__3___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_IR_UnboxResult_unboxAttr___lambda__3___closed__1;
x_2 = l_Lean_IR_UnboxResult_unboxAttr___lambda__3___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_IR_UnboxResult_unboxAttr___lambda__3___closed__1;
x_3 = l_Lean_IR_UnboxResult_unboxAttr___lambda__3___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_IR_UnboxResult_unboxAttr___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {

16
stage0/stdlib/Lean/Compiler/ImplementedByAttr.c generated
View file

@ -2775,13 +2775,15 @@ return x_2;
static lean_object* _init_l_Lean_Compiler_implementedByAttr___lambda__3___closed__2() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_implementedByAttr___lambda__3___closed__1;
x_2 = l_Lean_resolveGlobalConstNoOverload___at_Lean_Compiler_initFn____x40_Lean_Compiler_ImplementedByAttr___hyg_3____spec__3___closed__3;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Compiler_implementedByAttr___lambda__3___closed__1;
x_3 = l_Lean_resolveGlobalConstNoOverload___at_Lean_Compiler_initFn____x40_Lean_Compiler_ImplementedByAttr___hyg_3____spec__3___closed__3;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Compiler_implementedByAttr___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {

16
stage0/stdlib/Lean/Compiler/InitAttr.c generated
View file

@ -3599,13 +3599,15 @@ return x_2;
static lean_object* _init_l_Lean_registerInitAttr___rarg___closed__2() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_registerInitAttr___rarg___closed__1;
x_2 = l_Lean_resolveGlobalConstNoOverload___at_Lean_registerInitAttrUnsafe___spec__3___closed__3;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_registerInitAttr___rarg___closed__1;
x_3 = l_Lean_resolveGlobalConstNoOverload___at_Lean_registerInitAttrUnsafe___spec__3___closed__3;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_registerInitAttr___rarg(lean_object* x_1) {

16
stage0/stdlib/Lean/Compiler/InlineAttrs.c generated
View file

@ -2258,13 +2258,15 @@ return x_1;
static lean_object* _init_l_Lean_Compiler_inlineAttrs___lambda__1___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_inlineAttrs___lambda__1___closed__1;
x_2 = l_Lean_Compiler_inlineAttrs___lambda__1___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Compiler_inlineAttrs___lambda__1___closed__1;
x_3 = l_Lean_Compiler_inlineAttrs___lambda__1___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Compiler_inlineAttrs___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {

16
stage0/stdlib/Lean/Compiler/NeverExtractAttr.c generated
View file

@ -194,13 +194,15 @@ return x_1;
static lean_object* _init_l_Lean_neverExtractAttr___lambda__3___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_neverExtractAttr___lambda__3___closed__1;
x_2 = l_Lean_neverExtractAttr___lambda__3___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_neverExtractAttr___lambda__3___closed__1;
x_3 = l_Lean_neverExtractAttr___lambda__3___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_neverExtractAttr___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {

16
stage0/stdlib/Lean/Compiler/Specialize.c generated
View file

@ -2116,13 +2116,15 @@ return x_1;
static lean_object* _init_l_Lean_Compiler_specializeAttrs___lambda__1___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Compiler_specializeAttrs___lambda__1___closed__1;
x_2 = l_Lean_Compiler_specializeAttrs___lambda__1___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Compiler_specializeAttrs___lambda__1___closed__1;
x_3 = l_Lean_Compiler_specializeAttrs___lambda__1___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Compiler_specializeAttrs___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {

16
stage0/stdlib/Lean/DeclarationRange.c generated
View file

@ -1771,13 +1771,15 @@ return x_1;
static lean_object* _init_l_Lean_declRangeExt___elambda__4___rarg___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_declRangeExt___elambda__4___rarg___closed__1;
x_2 = l_Lean_declRangeExt___elambda__4___rarg___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_declRangeExt___elambda__4___rarg___closed__1;
x_3 = l_Lean_declRangeExt___elambda__4___rarg___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_declRangeExt___elambda__4___rarg(lean_object* x_1) {

16
stage0/stdlib/Lean/DocString.c generated
View file

@ -1106,13 +1106,15 @@ return x_1;
static lean_object* _init_l_Lean_docStringExt___elambda__4___rarg___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_docStringExt___elambda__4___rarg___closed__1;
x_2 = l_Lean_docStringExt___elambda__4___rarg___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_docStringExt___elambda__4___rarg___closed__1;
x_3 = l_Lean_docStringExt___elambda__4___rarg___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_docStringExt___elambda__4___rarg(lean_object* x_1) {

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

@ -937,13 +937,15 @@ return x_1;
static lean_object* _init_l_Lean_Elab_Term_elabWithoutExpectedTypeAttr___lambda__3___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_elabWithoutExpectedTypeAttr___lambda__3___closed__1;
x_2 = l_Lean_Elab_Term_elabWithoutExpectedTypeAttr___lambda__3___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_Term_elabWithoutExpectedTypeAttr___lambda__3___closed__1;
x_3 = l_Lean_Elab_Term_elabWithoutExpectedTypeAttr___lambda__3___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Elab_Term_elabWithoutExpectedTypeAttr___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {

16
stage0/stdlib/Lean/Elab/Command.c generated
View file

@ -6593,13 +6593,15 @@ return x_8;
static lean_object* _init_l_Lean_Elab_Command_mkCommandElabAttribute___closed__1() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Command_instInhabitedState___closed__3;
x_2 = l_Lean_Elab_Command_instInhabitedScope___closed__1;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_Command_instInhabitedState___closed__3;
x_3 = l_Lean_Elab_Command_instInhabitedScope___closed__1;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Elab_Command_mkCommandElabAttribute(lean_object* x_1) {

16
stage0/stdlib/Lean/Elab/Quotation/Precheck.c generated
View file

@ -755,13 +755,15 @@ return x_2;
static lean_object* _init_l_Lean_Elab_Term_Quotation_precheckAttribute___lambda__2___closed__2() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_Quotation_precheckAttribute___lambda__2___closed__1;
x_2 = l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation_Precheck___hyg_75____closed__3;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_Term_Quotation_precheckAttribute___lambda__2___closed__1;
x_3 = l_Lean_Elab_Term_Quotation_initFn____x40_Lean_Elab_Quotation_Precheck___hyg_75____closed__3;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Elab_Term_Quotation_precheckAttribute___lambda__2(lean_object* x_1) {

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

File diff suppressed because it is too large Load diff

6
stage0/stdlib/Lean/Elab/Structure.c generated
View file

@ -619,7 +619,7 @@ lean_object* l_Lean_Elab_getOptDerivingClasses___at_Lean_Elab_Command_elabStruct
static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___rarg___closed__10;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabStructure___spec__11(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__17___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_5182_(lean_object*);
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_5176_(lean_object*);
lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___rarg___closed__20;
uint8_t l___private_Lean_Expr_0__Lean_beqBinderInfo____x40_Lean_Expr___hyg_234_(uint8_t, uint8_t);
@ -21843,7 +21843,7 @@ lean_dec(x_8);
return x_15;
}
}
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_5182_(lean_object* x_1) {
lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_5176_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -22293,7 +22293,7 @@ l_Lean_Elab_Command_elabStructure___closed__9 = _init_l_Lean_Elab_Command_elabSt
lean_mark_persistent(l_Lean_Elab_Command_elabStructure___closed__9);
l_Lean_Elab_Command_elabStructure___closed__10 = _init_l_Lean_Elab_Command_elabStructure___closed__10();
lean_mark_persistent(l_Lean_Elab_Command_elabStructure___closed__10);
res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_5182_(lean_io_mk_world());
res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Structure___hyg_5176_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));

16
stage0/stdlib/Lean/Elab/Tactic/Basic.c generated
View file

@ -3071,13 +3071,15 @@ return x_2;
static lean_object* _init_l_Lean_Elab_Tactic_tacticElabAttribute___lambda__2___closed__2() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Tactic_tacticElabAttribute___lambda__2___closed__1;
x_2 = l_Lean_Elab_Term_reportUnsolvedGoals___closed__7;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_Tactic_tacticElabAttribute___lambda__2___closed__1;
x_3 = l_Lean_Elab_Term_reportUnsolvedGoals___closed__7;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Elab_Tactic_tacticElabAttribute___lambda__2(lean_object* x_1) {

16
stage0/stdlib/Lean/Elab/Term.c generated
View file

@ -8382,13 +8382,15 @@ return x_1;
static lean_object* _init_l_Lean_Elab_Term_mkTermElabAttribute___closed__2() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_instInhabitedSavedState___closed__3;
x_2 = l_Lean_Elab_Term_mkTermElabAttribute___closed__1;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_Term_instInhabitedSavedState___closed__3;
x_3 = l_Lean_Elab_Term_mkTermElabAttribute___closed__1;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Elab_Term_mkTermElabAttribute(lean_object* x_1) {

16
stage0/stdlib/Lean/Elab/Util.c generated
View file

@ -1755,13 +1755,15 @@ return x_2;
static lean_object* _init_l_Lean_Elab_mkMacroAttribute___closed__2() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_mkMacroAttribute___closed__1;
x_2 = l_Lean_Elab_evalSyntaxConstant___closed__1;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_mkMacroAttribute___closed__1;
x_3 = l_Lean_Elab_evalSyntaxConstant___closed__1;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Elab_mkMacroAttribute(lean_object* x_1) {

16
stage0/stdlib/Lean/Environment.c generated
View file

@ -3340,13 +3340,15 @@ return x_5;
static lean_object* _init_l_Lean_EnvExtensionInterfaceUnsafe_instInhabitedExt___lambda__1___closed__1() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_instInhabitedEnvironmentHeader___closed__1;
x_2 = l_Lean_instToStringImport___closed__1;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_instInhabitedEnvironmentHeader___closed__1;
x_3 = l_Lean_instToStringImport___closed__1;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_EnvExtensionInterfaceUnsafe_instInhabitedExt___lambda__1(lean_object* x_1) {

16
stage0/stdlib/Lean/KeyedDeclsAttribute.c generated
View file

@ -672,13 +672,15 @@ return x_2;
static lean_object* _init_l_Lean_instInhabitedKeyedDeclsAttribute___lambda__1___closed__2() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_instInhabitedKeyedDeclsAttribute___lambda__1___closed__1;
x_2 = l_Lean_KeyedDeclsAttribute_instInhabitedDef___closed__1;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_instInhabitedKeyedDeclsAttribute___lambda__1___closed__1;
x_3 = l_Lean_KeyedDeclsAttribute_instInhabitedDef___closed__1;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_instInhabitedKeyedDeclsAttribute___lambda__1(lean_object* x_1) {

16
stage0/stdlib/Lean/Meta/Instances.c generated
View file

@ -2281,13 +2281,15 @@ return x_1;
static lean_object* _init_l_Lean_Meta_instanceExtension___lambda__1___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_instanceExtension___lambda__1___closed__1;
x_2 = l_Lean_Meta_instanceExtension___lambda__1___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_instanceExtension___lambda__1___closed__1;
x_3 = l_Lean_Meta_instanceExtension___lambda__1___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Meta_instanceExtension___lambda__1(lean_object* x_1) {

16
stage0/stdlib/Lean/Meta/Match/MatchPatternAttr.c generated
View file

@ -190,13 +190,15 @@ return x_1;
static lean_object* _init_l_Lean_matchPatternAttr___lambda__3___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_matchPatternAttr___lambda__3___closed__1;
x_2 = l_Lean_matchPatternAttr___lambda__3___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_matchPatternAttr___lambda__3___closed__1;
x_3 = l_Lean_matchPatternAttr___lambda__3___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_matchPatternAttr___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {

16
stage0/stdlib/Lean/Meta/Match/MatcherInfo.c generated
View file

@ -2218,13 +2218,15 @@ return x_1;
static lean_object* _init_l_Lean_Meta_Match_Extension_extension___elambda__4___rarg___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Match_Extension_extension___elambda__4___rarg___closed__1;
x_2 = l_Lean_Meta_Match_Extension_extension___elambda__4___rarg___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Match_Extension_extension___elambda__4___rarg___closed__1;
x_3 = l_Lean_Meta_Match_Extension_extension___elambda__4___rarg___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Meta_Match_Extension_extension___elambda__4___rarg(lean_object* x_1) {

16
stage0/stdlib/Lean/Meta/RecursorInfo.c generated
View file

@ -11472,13 +11472,15 @@ return x_2;
static lean_object* _init_l_Lean_Meta_recursorAttribute___lambda__3___closed__2() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_recursorAttribute___lambda__3___closed__1;
x_2 = l_List_toStringAux___at_Lean_Meta_RecursorInfo_instToStringRecursorInfo___spec__2___closed__1;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_recursorAttribute___lambda__3___closed__1;
x_3 = l_List_toStringAux___at_Lean_Meta_RecursorInfo_instToStringRecursorInfo___spec__2___closed__1;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Meta_recursorAttribute___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {

16
stage0/stdlib/Lean/Meta/SynthInstance.c generated
View file

@ -887,13 +887,15 @@ return x_2;
static lean_object* _init_l_Lean_Meta_SynthInstance_inferTCGoalsRLAttr___lambda__3___closed__2() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_SynthInstance_inferTCGoalsRLAttr___lambda__3___closed__1;
x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4____closed__5;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_SynthInstance_inferTCGoalsRLAttr___lambda__3___closed__1;
x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_SynthInstance___hyg_4____closed__5;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Meta_SynthInstance_inferTCGoalsRLAttr___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {

16
stage0/stdlib/Lean/Meta/Tactic/Simp/CongrLemmas.c generated
View file

@ -4036,13 +4036,15 @@ return x_1;
static lean_object* _init_l_Lean_Meta_congrExtension___lambda__1___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_congrExtension___lambda__1___closed__1;
x_2 = l_Lean_Meta_congrExtension___lambda__1___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_congrExtension___lambda__1___closed__1;
x_3 = l_Lean_Meta_congrExtension___lambda__1___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Meta_congrExtension___lambda__1(lean_object* x_1) {

16
stage0/stdlib/Lean/Meta/Tactic/Simp/SimpLemmas.c generated
View file

@ -4366,13 +4366,15 @@ return x_2;
static lean_object* _init_l_Lean_Meta_simpExtension___lambda__1___closed__2() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_simpExtension___lambda__1___closed__1;
x_2 = l_Lean_Meta_instToFormatSimpLemma___closed__3;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_simpExtension___lambda__1___closed__1;
x_3 = l_Lean_Meta_instToFormatSimpLemma___closed__3;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Meta_simpExtension___lambda__1(lean_object* x_1) {

16
stage0/stdlib/Lean/Meta/UnificationHint.c generated
View file

@ -2893,13 +2893,15 @@ return x_1;
static lean_object* _init_l_Lean_Meta_unificationHintExtension___lambda__1___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_unificationHintExtension___lambda__1___closed__1;
x_2 = l_Lean_Meta_unificationHintExtension___lambda__1___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_unificationHintExtension___lambda__1___closed__1;
x_3 = l_Lean_Meta_unificationHintExtension___lambda__1___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Meta_unificationHintExtension___lambda__1(lean_object* x_1) {

16
stage0/stdlib/Lean/Modifiers.c generated
View file

@ -147,13 +147,15 @@ return x_1;
static lean_object* _init_l_Lean_protectedExt___elambda__4___rarg___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_protectedExt___elambda__4___rarg___closed__1;
x_2 = l_Lean_protectedExt___elambda__4___rarg___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_protectedExt___elambda__4___rarg___closed__1;
x_3 = l_Lean_protectedExt___elambda__4___rarg___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_protectedExt___elambda__4___rarg(lean_object* x_1) {

730
stage0/stdlib/Lean/Parser/Command.c generated
View file

File diff suppressed because it is too large Load diff

16
stage0/stdlib/Lean/Parser/Extension.c generated
View file

@ -5819,13 +5819,15 @@ return x_2;
static lean_object* _init_l_Lean_Parser_mkParserOfConstantAux___rarg___closed__2() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_mkParserOfConstantAux___rarg___closed__1;
x_2 = l_Lean_Parser_ParserExtension_instInhabitedOLeanEntry___closed__1;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_mkParserOfConstantAux___rarg___closed__1;
x_3 = l_Lean_Parser_ParserExtension_instInhabitedOLeanEntry___closed__1;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Parser_mkParserOfConstantAux___rarg(lean_object* x_1) {

16
stage0/stdlib/Lean/ParserCompiler/Attribute.c generated
View file

@ -224,13 +224,15 @@ return x_1;
static lean_object* _init_l_Lean_ParserCompiler_instInhabitedCombinatorAttribute___lambda__3___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_ParserCompiler_instInhabitedCombinatorAttribute___lambda__3___closed__1;
x_2 = l_Lean_ParserCompiler_instInhabitedCombinatorAttribute___lambda__3___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_ParserCompiler_instInhabitedCombinatorAttribute___lambda__3___closed__1;
x_3 = l_Lean_ParserCompiler_instInhabitedCombinatorAttribute___lambda__3___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_ParserCompiler_instInhabitedCombinatorAttribute___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {

16
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Basic.c generated
View file

@ -3381,13 +3381,15 @@ return x_1;
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabAttribute___lambda__2___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_PrettyPrinter_Delaborator_delabAttribute___lambda__2___closed__1;
x_2 = l_Lean_PrettyPrinter_Delaborator_delabAttribute___lambda__2___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_PrettyPrinter_Delaborator_delabAttribute___lambda__2___closed__1;
x_3 = l_Lean_PrettyPrinter_Delaborator_delabAttribute___lambda__2___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_PrettyPrinter_Delaborator_delabAttribute___lambda__2(lean_object* x_1) {

16
stage0/stdlib/Lean/PrettyPrinter/Formatter.c generated
View file

@ -1292,13 +1292,15 @@ return x_2;
static lean_object* _init_l_Lean_PrettyPrinter_formatterAttribute___lambda__2___closed__2() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_PrettyPrinter_formatterAttribute___lambda__2___closed__1;
x_2 = l_Lean_PrettyPrinter_Formatter_State_leadWord___default___closed__1;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_PrettyPrinter_formatterAttribute___lambda__2___closed__1;
x_3 = l_Lean_PrettyPrinter_Formatter_State_leadWord___default___closed__1;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_PrettyPrinter_formatterAttribute___lambda__2(lean_object* x_1) {

16
stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c generated
View file

@ -1429,13 +1429,15 @@ return x_1;
static lean_object* _init_l_Lean_PrettyPrinter_parenthesizerAttribute___lambda__2___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_PrettyPrinter_parenthesizerAttribute___lambda__2___closed__1;
x_2 = l_Lean_PrettyPrinter_parenthesizerAttribute___lambda__2___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_PrettyPrinter_parenthesizerAttribute___lambda__2___closed__1;
x_3 = l_Lean_PrettyPrinter_parenthesizerAttribute___lambda__2___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute___lambda__2(lean_object* x_1) {

16
stage0/stdlib/Lean/ProjFns.c generated
View file

@ -1187,13 +1187,15 @@ return x_1;
static lean_object* _init_l_Lean_projectionFnInfoExt___elambda__4___rarg___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_projectionFnInfoExt___elambda__4___rarg___closed__1;
x_2 = l_Lean_projectionFnInfoExt___elambda__4___rarg___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_projectionFnInfoExt___elambda__4___rarg___closed__1;
x_3 = l_Lean_projectionFnInfoExt___elambda__4___rarg___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_projectionFnInfoExt___elambda__4___rarg(lean_object* x_1) {

16
stage0/stdlib/Lean/ReducibilityAttrs.c generated
View file

@ -2269,13 +2269,15 @@ return x_1;
static lean_object* _init_l_Lean_reducibilityAttrs___lambda__1___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_reducibilityAttrs___lambda__1___closed__1;
x_2 = l_Lean_reducibilityAttrs___lambda__1___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_reducibilityAttrs___lambda__1___closed__1;
x_3 = l_Lean_reducibilityAttrs___lambda__1___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_reducibilityAttrs___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {

16
stage0/stdlib/Lean/ResolveName.c generated
View file

@ -2585,13 +2585,15 @@ return x_1;
static lean_object* _init_l_Lean_aliasExtension___elambda__4___rarg___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_aliasExtension___elambda__4___rarg___closed__1;
x_2 = l_Lean_aliasExtension___elambda__4___rarg___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_aliasExtension___elambda__4___rarg___closed__1;
x_3 = l_Lean_aliasExtension___elambda__4___rarg___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_aliasExtension___elambda__4___rarg(lean_object* x_1) {

16
stage0/stdlib/Lean/ScopedEnvExtension.c generated
View file

@ -737,13 +737,15 @@ return x_1;
static lean_object* _init_l_Lean_ScopedEnvExtension_instInhabitedDescr___rarg___lambda__1___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_ScopedEnvExtension_instInhabitedDescr___rarg___lambda__1___closed__1;
x_2 = l_Lean_ScopedEnvExtension_instInhabitedDescr___rarg___lambda__1___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_ScopedEnvExtension_instInhabitedDescr___rarg___lambda__1___closed__1;
x_3 = l_Lean_ScopedEnvExtension_instInhabitedDescr___rarg___lambda__1___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_ScopedEnvExtension_instInhabitedDescr___rarg___lambda__1(lean_object* x_1) {

16
stage0/stdlib/Lean/Server/Completion.c generated
View file

@ -488,13 +488,15 @@ return x_1;
static lean_object* _init_l_Lean_Server_Completion_completionBlackListExt___elambda__4___rarg___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Server_Completion_completionBlackListExt___elambda__4___rarg___closed__1;
x_2 = l_Lean_Server_Completion_completionBlackListExt___elambda__4___rarg___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Server_Completion_completionBlackListExt___elambda__4___rarg___closed__1;
x_3 = l_Lean_Server_Completion_completionBlackListExt___elambda__4___rarg___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_Server_Completion_completionBlackListExt___elambda__4___rarg(lean_object* x_1) {

16
stage0/stdlib/Lean/Util/PPExt.c generated
View file

@ -532,13 +532,15 @@ return x_1;
static lean_object* _init_l_Lean_instInhabitedPPFns___lambda__1___closed__3() {
_start:
{
uint32_t x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_instInhabitedPPFns___lambda__1___closed__1;
x_2 = l_Lean_instInhabitedPPFns___lambda__1___closed__2;
x_3 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set_uint32(x_3, sizeof(void*)*1, x_1);
return x_3;
lean_object* x_1; uint32_t x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_instInhabitedPPFns___lambda__1___closed__1;
x_3 = l_Lean_instInhabitedPPFns___lambda__1___closed__2;
x_4 = lean_alloc_ctor(0, 2, 4);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set_uint32(x_4, sizeof(void*)*2, x_2);
return x_4;
}
}
lean_object* l_Lean_instInhabitedPPFns___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {