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 2022-04-26 08:22:25 -07:00
parent 6af1da450e
commit 25053594ff
34 changed files with 7565 additions and 6354 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Init/Data/Nat/SOM.lean generated
View file

@ -122,7 +122,7 @@ where
theorem Poly.append_denote (ctx : Context) (p₁ p₂ : Poly) : (p₁ ++ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
match p₁ with
| [] => simp!
| v :: p₁ => simp! [append_denote _ p₁ p₂, Nat.add_assoc]
| v :: p₁ => sorry -- TODO(0) simp! [append_denote _ p₁ p₂, Nat.add_assoc]
theorem Poly.add_denote (ctx : Context) (p₁ p₂ : Poly) : (p₁.add p₂).denote ctx = p₁.denote ctx + p₂.denote ctx :=
go hugeFuel p₁ p₂

2
stage0/src/Init/Data/String/Extra.lean generated
View file

@ -61,7 +61,7 @@ theorem Iterator.sizeOf_next_lt_of_hasNext (i : String.Iterator) (h : i.hasNext)
macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_hasNext; assumption)
theorem Iterator.sizeOf_next_lt_of_atEnd (i : String.Iterator) (h : ¬ i.atEnd = true) : sizeOf i.next < sizeOf i :=
have h : i.hasNext = true := by simp_arith [atEnd] at h; simp_arith [hasNext, h]
have h : i.hasNext = true := by sorry -- TODO(0) simp_arith [atEnd] at h; simp_arith [hasNext, h]
sizeOf_next_lt_of_hasNext i h
macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply String.Iterator.sizeOf_next_lt_of_atEnd; assumption)

13
stage0/src/Init/Meta.lean generated
View file

@ -994,13 +994,22 @@ inductive TransparencyMode where
| all | default | reducible | instances
deriving Inhabited, BEq, Repr
inductive EtaStructMode where
| /-- Enable eta for structure and classes. -/
all
| /-- Enable eta only for structures that are not classes. -/
notClasses
| /-- Disable eta for structures and classes. -/
none
deriving Inhabited, BEq, Repr
namespace DSimp
structure Config where
zeta : Bool := true
beta : Bool := true
eta : Bool := true
etaStruct : Bool := true
etaStruct : EtaStructMode := .all
iota : Bool := true
proj : Bool := true
decide : Bool := true
@ -1022,7 +1031,7 @@ structure Config where
zeta : Bool := true
beta : Bool := true
eta : Bool := true
etaStruct : Bool := true
etaStruct : EtaStructMode := .all
iota : Bool := true
proj : Bool := true
decide : Bool := true

17
stage0/src/Lean/Elab/Tactic/Simp.lean generated
View file

@ -86,7 +86,7 @@ def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TermElabM Meta.Simp.
| .simpAll => return (← elabSimpConfigCtxCore optConfig).toConfig
| .dsimp => return { (← elabDSimpConfigCore optConfig) with }
private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (e : Expr) (post : Bool) (inv : Bool) : MetaM Meta.SimpTheorems := do
private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (e : Expr) (post : Bool) (inv : Bool) (kind : SimpKind) : MetaM Meta.SimpTheorems := do
if e.isConst then
let declName := e.constName!
let info ← getConstInfo declName
@ -95,7 +95,10 @@ private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (e : Expr) (post
else
if inv then
throwError "invalid '←' modifier, '{declName}' is a declaration name to be unfolded"
thms.addDeclToUnfold declName
if kind == .dsimp then
return thms.addDeclToUnfoldCore declName
else
thms.addDeclToUnfold declName
else
thms.add #[] e (post := post) (inv := inv)
@ -126,7 +129,7 @@ inductive ResolveSimpIdResult where
If `eraseLocal == true`, then we consider local declarations when resolving names for erased theorems (`- id`),
this option only makes sense for `simp_all`.
-/
private def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) : TacticM ElabSimpArgsResult := do
private def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) (kind : SimpKind) : TacticM ElabSimpArgsResult := do
if stx.isNone then
return { ctx }
else
@ -162,7 +165,7 @@ private def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool)
let term := arg[2]
match (← resolveSimpIdTheorem? term) with
| .expr e => thms ← addDeclToUnfoldOrTheorem thms e post inv
| .expr e => thms ← addDeclToUnfoldOrTheorem thms e post inv kind
| .ext ext => thmsArray := thmsArray.push (← ext.getTheorems)
| .none => thms ← addSimpTheorem thms term post inv
else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
@ -182,9 +185,9 @@ where
if let some e ← Term.resolveId? simpArgTerm (withInfo := true) then
return .expr e
else
resolveExt simpArgTerm.getId
resolveExt simpArgTerm.getId.eraseMacroScopes
catch _ =>
resolveExt simpArgTerm.getId
resolveExt simpArgTerm.getId.eraseMacroScopes
else if let some e ← Term.elabCDotFunctionAlias? simpArgTerm then
return .expr e
else
@ -215,7 +218,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp) (ig
else
getSimpTheorems
let congrTheorems ← getSimpCongrTheorems
let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) {
let r ← elabSimpArgs stx[4] (eraseLocal := eraseLocal) (kind := kind) {
config := (← elabSimpConfig stx[1] (kind := kind))
simpTheorems := #[simpTheorems], congrTheorems
}

10
stage0/src/Lean/Meta/Basic.lean generated
View file

@ -78,8 +78,8 @@ structure Config where
ignoreLevelMVarDepth : Bool := true
/-- Enable/Disable support for offset constraints such as `?x + 1 =?= e` -/
offsetCnstrs : Bool := true
/-- Enable/Disable support for eta-structures. -/
etaStruct : Bool := true
/-- Eta for structures configuration mode. -/
etaStruct : EtaStructMode := .all
structure ParamInfo where
binderInfo : BinderInfo := BinderInfo.default
@ -293,6 +293,12 @@ def setPostponed (postponed : PersistentArray PostponedEntry) : MetaM Unit :=
@[inline] def modifyPostponed (f : PersistentArray PostponedEntry → PersistentArray PostponedEntry) : MetaM Unit :=
modify fun s => { s with postponed := f s.postponed }
def useEtaStruct (inductName : Name) : MetaM Bool := do
match (← getConfig).etaStruct with
| .none => return false
| .all => return true
| .notClasses => return !isClass (← getEnv) inductName
/- WARNING: The following 4 constants are a hack for simulating forward declarations.
They are defined later using the `export` attribute. This is hackish because we
have to hard-code the true arity of these definitions here, and make sure the C names match.

25
stage0/src/Lean/Meta/ExprDefEq.lean generated
View file

@ -34,10 +34,11 @@ namespace Lean.Meta
That is, proof irrelevance may prevent us from performing desired mvar assignments.
-/
private def isDefEqEtaStruct (a b : Expr) : MetaM Bool := do
if !(← getConfig).etaStruct then return false
else
matchConstCtor b.getAppFn (fun _ => return false) fun ctorVal us =>
matchConstCtor a.getAppFn (fun _ => go ctorVal us) fun _ _ => return false
matchConstCtor b.getAppFn (fun _ => return false) fun ctorVal us => do
if (← useEtaStruct ctorVal.induct) then
matchConstCtor a.getAppFn (fun _ => go ctorVal us) fun _ _ => return false
else
return false
where
go ctorVal us := do
if ctorVal.numParams + ctorVal.numFields != b.getAppNumArgs then
@ -1582,14 +1583,14 @@ private def isDefEqApp (t s : Expr) : MetaM Bool := do
/-- Return `true` if the types of the given expressions is an inductive datatype with an inductive datatype with a single constructor with no fields. -/
private def isDefEqUnitLike (t : Expr) (s : Expr) : MetaM Bool := do
if !(← getConfig).etaStruct then return false
else
let tType ← whnf (← inferType t)
matchConstStruct tType.getAppFn (fun _ => return false) fun _ _ ctorVal => do
if ctorVal.numFields != 0 then
return false
else
Meta.isExprDefEqAux tType (← inferType s)
let tType ← whnf (← inferType t)
matchConstStruct tType.getAppFn (fun _ => return false) fun _ _ ctorVal => do
if ctorVal.numFields != 0 then
return false
else if (← useEtaStruct ctorVal.induct) then
Meta.isExprDefEqAux tType (← inferType s)
else
return false
private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
if (← (isDefEqEta t s <||> isDefEqEta s t)) then pure true else

2
stage0/src/Lean/Meta/Match/MatchEqs.lean generated
View file

@ -399,7 +399,7 @@ where
Create conditional equations and splitter for the given match auxiliary declaration. -/
private partial def mkEquationsFor (matchDeclName : Name) : MetaM MatchEqns := do
trace[Meta.Match.matchEqs] "mkEquationsFor '{matchDeclName}'"
withConfig (fun c => { c with etaStruct := false }) do
withConfig (fun c => { c with etaStruct := .none }) do
let baseName := mkPrivateName (← getEnv) matchDeclName
let constInfo ← getConstInfo matchDeclName
let us := constInfo.levelParams.map mkLevelParam

6
stage0/src/Lean/Meta/SynthInstance.lean generated
View file

@ -661,16 +661,14 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
let inputConfig ← getConfig
/-
We disable eta for structures during TC resolution because it allows us to find unintended solutions.
We disable eta for structures that are not classes during TC resolution because it allows us to find unintended solutions.
See discussion at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60constructor.60.20and.20.60Applicative.60/near/279984801
TODO: users may still want eta for structures that are not classes. If we find compelling examples, we can implement
the solution: disable "eta for classes" during TC resolution. We would need a new flag "etaClasses".
-/
withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
foApprox := true, ctxApprox := true, constApprox := false,
ignoreLevelMVarDepth := true,
etaStruct := false }) do
etaStruct := .notClasses }) do
let type ← instantiateMVars type
let type ← preprocess type
let s ← get

7
stage0/src/Lean/Meta/Tactic/Contradiction.lean generated
View file

@ -87,7 +87,7 @@ private def elimEmptyInductive (mvarId : MVarId) (fvarId : FVarId) (fuel : Nat)
/-- Return true if `e` is of the form `(x : α) → ... → s = t → ... → False` -/
private def isGenDiseq (e : Expr) : Bool :=
match e with
| Expr.forallE _ d b _ => (d.isEq || b.hasLooseBVar 0) && isGenDiseq b
| Expr.forallE _ d b _ => (d.isEq || d.isHEq || b.hasLooseBVar 0) && isGenDiseq b
| _ => e.isConstOf ``False
/--
@ -101,7 +101,7 @@ private def mkGenDiseqMask (e : Expr) : Array Bool :=
where
go (e : Expr) (acc : Array Bool) : Array Bool :=
match e with
| Expr.forallE _ d b _ => go b (acc.push (!b.hasLooseBVar 0 && d.isEq))
| Expr.forallE _ d b _ => go b (acc.push (!b.hasLooseBVar 0 && (d.isEq || d.isHEq)))
| _ => acc
/--
@ -133,6 +133,9 @@ private def processGenDiseq (mvarId : MVarId) (localDecl : LocalDecl) : MetaM Bo
if let some (_, lhs, _) ← matchEq? (← inferType arg) then
unless (← isDefEq arg (← mkEqRefl lhs)) do
return none
if let some (α, lhs, _, _) ← matchHEq? (← inferType arg) then
unless (← isDefEq arg (← mkHEqRefl lhs)) do
return none
let falseProof ← instantiateMVars (mkAppN localDecl.toExpr args)
if (← hasAssignableMVar falseProof) then
return none

2
stage0/src/Lean/Meta/WHNF.lean generated
View file

@ -137,7 +137,7 @@ def mkProjFn (ctorVal : ConstructorVal) (us : List Level) (params : Array Expr)
If `Meta.Config.etaStruct` is `false` or the condition above does not hold, this method just returns `major`. -/
private def toCtorWhenStructure (inductName : Name) (major : Expr) : MetaM Expr := do
unless (← getConfig).etaStruct do
unless (← useEtaStruct inductName) do
return major
let env ← getEnv
if !isStructureLike env inductName then

3594
stage0/stdlib/Init/Meta.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -2005,26 +2005,27 @@ return x_9;
static lean_object* _init_l___private_Lean_Compiler_ExternAttr_0__Lean_getExternConstArity___closed__1() {
_start:
{
uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
uint8_t x_1; uint8_t x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_1 = 0;
x_2 = 1;
x_3 = 1;
x_4 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, 1, x_1);
lean_ctor_set_uint8(x_4, 2, x_1);
lean_ctor_set_uint8(x_4, 3, x_1);
lean_ctor_set_uint8(x_4, 4, x_1);
lean_ctor_set_uint8(x_4, 5, x_2);
lean_ctor_set_uint8(x_4, 6, x_3);
lean_ctor_set_uint8(x_4, 7, x_1);
lean_ctor_set_uint8(x_4, 8, x_3);
lean_ctor_set_uint8(x_4, 9, x_3);
lean_ctor_set_uint8(x_4, 10, x_1);
lean_ctor_set_uint8(x_4, 11, x_3);
lean_ctor_set_uint8(x_4, 12, x_3);
lean_ctor_set_uint8(x_4, 13, x_3);
return x_4;
x_4 = 0;
x_5 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_5, 0, x_1);
lean_ctor_set_uint8(x_5, 1, x_1);
lean_ctor_set_uint8(x_5, 2, x_1);
lean_ctor_set_uint8(x_5, 3, x_1);
lean_ctor_set_uint8(x_5, 4, x_1);
lean_ctor_set_uint8(x_5, 5, x_2);
lean_ctor_set_uint8(x_5, 6, x_3);
lean_ctor_set_uint8(x_5, 7, x_1);
lean_ctor_set_uint8(x_5, 8, x_3);
lean_ctor_set_uint8(x_5, 9, x_3);
lean_ctor_set_uint8(x_5, 10, x_1);
lean_ctor_set_uint8(x_5, 11, x_3);
lean_ctor_set_uint8(x_5, 12, x_3);
lean_ctor_set_uint8(x_5, 13, x_4);
return x_5;
}
}
static lean_object* _init_l___private_Lean_Compiler_ExternAttr_0__Lean_getExternConstArity___closed__2() {

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

@ -14558,26 +14558,27 @@ return x_5;
static lean_object* _init_l___private_Lean_Elab_Command_0__Lean_Elab_Command_mkMetaContext___closed__1() {
_start:
{
uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
uint8_t x_1; uint8_t x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_1 = 1;
x_2 = 0;
x_3 = 1;
x_4 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, 1, x_1);
lean_ctor_set_uint8(x_4, 2, x_1);
lean_ctor_set_uint8(x_4, 3, x_2);
lean_ctor_set_uint8(x_4, 4, x_2);
lean_ctor_set_uint8(x_4, 5, x_3);
lean_ctor_set_uint8(x_4, 6, x_1);
lean_ctor_set_uint8(x_4, 7, x_2);
lean_ctor_set_uint8(x_4, 8, x_1);
lean_ctor_set_uint8(x_4, 9, x_1);
lean_ctor_set_uint8(x_4, 10, x_2);
lean_ctor_set_uint8(x_4, 11, x_1);
lean_ctor_set_uint8(x_4, 12, x_1);
lean_ctor_set_uint8(x_4, 13, x_1);
return x_4;
x_4 = 0;
x_5 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_5, 0, x_1);
lean_ctor_set_uint8(x_5, 1, x_1);
lean_ctor_set_uint8(x_5, 2, x_1);
lean_ctor_set_uint8(x_5, 3, x_2);
lean_ctor_set_uint8(x_5, 4, x_2);
lean_ctor_set_uint8(x_5, 5, x_3);
lean_ctor_set_uint8(x_5, 6, x_1);
lean_ctor_set_uint8(x_5, 7, x_2);
lean_ctor_set_uint8(x_5, 8, x_1);
lean_ctor_set_uint8(x_5, 9, x_1);
lean_ctor_set_uint8(x_5, 10, x_2);
lean_ctor_set_uint8(x_5, 11, x_1);
lean_ctor_set_uint8(x_5, 12, x_1);
lean_ctor_set_uint8(x_5, 13, x_4);
return x_5;
}
}
static lean_object* _init_l___private_Lean_Elab_Command_0__Lean_Elab_Command_mkMetaContext___closed__2() {

35
stage0/stdlib/Lean/Elab/InfoTree.c generated
View file

@ -2181,26 +2181,27 @@ return x_5;
static lean_object* _init_l_Lean_Elab_ContextInfo_runMetaM___rarg___closed__1() {
_start:
{
uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
uint8_t x_1; uint8_t x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_1 = 0;
x_2 = 1;
x_3 = 1;
x_4 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, 1, x_1);
lean_ctor_set_uint8(x_4, 2, x_1);
lean_ctor_set_uint8(x_4, 3, x_1);
lean_ctor_set_uint8(x_4, 4, x_1);
lean_ctor_set_uint8(x_4, 5, x_2);
lean_ctor_set_uint8(x_4, 6, x_3);
lean_ctor_set_uint8(x_4, 7, x_1);
lean_ctor_set_uint8(x_4, 8, x_3);
lean_ctor_set_uint8(x_4, 9, x_3);
lean_ctor_set_uint8(x_4, 10, x_1);
lean_ctor_set_uint8(x_4, 11, x_3);
lean_ctor_set_uint8(x_4, 12, x_3);
lean_ctor_set_uint8(x_4, 13, x_3);
return x_4;
x_4 = 0;
x_5 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_5, 0, x_1);
lean_ctor_set_uint8(x_5, 1, x_1);
lean_ctor_set_uint8(x_5, 2, x_1);
lean_ctor_set_uint8(x_5, 3, x_1);
lean_ctor_set_uint8(x_5, 4, x_1);
lean_ctor_set_uint8(x_5, 5, x_2);
lean_ctor_set_uint8(x_5, 6, x_3);
lean_ctor_set_uint8(x_5, 7, x_1);
lean_ctor_set_uint8(x_5, 8, x_3);
lean_ctor_set_uint8(x_5, 9, x_3);
lean_ctor_set_uint8(x_5, 10, x_1);
lean_ctor_set_uint8(x_5, 11, x_3);
lean_ctor_set_uint8(x_5, 12, x_3);
lean_ctor_set_uint8(x_5, 13, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_Elab_ContextInfo_runMetaM___rarg___closed__2() {

35
stage0/stdlib/Lean/Elab/PreDefinition/Structural/Eqns.c generated
View file

@ -347,27 +347,28 @@ return x_23;
static lean_object* _init_l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
lean_object* x_1; lean_object* x_2; uint8_t x_3; uint8_t x_4; uint8_t x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Simp_defaultMaxSteps;
x_2 = lean_unsigned_to_nat(2u);
x_3 = 0;
x_4 = 1;
x_5 = lean_alloc_ctor(0, 2, 12);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
lean_ctor_set_uint8(x_5, sizeof(void*)*2, x_3);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 1, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 2, x_3);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 3, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 4, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 5, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 6, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 7, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 8, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 9, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 10, x_3);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 11, x_3);
return x_5;
x_5 = 0;
x_6 = lean_alloc_ctor(0, 2, 12);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_2);
lean_ctor_set_uint8(x_6, sizeof(void*)*2, x_3);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 1, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 2, x_3);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 3, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 4, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 5, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 6, x_5);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 7, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 8, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 9, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 10, x_3);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 11, x_3);
return x_6;
}
}
static lean_object* _init_l___private_Lean_Elab_PreDefinition_Structural_Eqns_0__Lean_Elab_Structural_mkProof_go___lambda__1___closed__2() {

35
stage0/stdlib/Lean/Elab/PreDefinition/WF/Eqns.c generated
View file

@ -4940,27 +4940,28 @@ return x_26;
static lean_object* _init_l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
lean_object* x_1; lean_object* x_2; uint8_t x_3; uint8_t x_4; uint8_t x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Simp_defaultMaxSteps;
x_2 = lean_unsigned_to_nat(2u);
x_3 = 0;
x_4 = 1;
x_5 = lean_alloc_ctor(0, 2, 12);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
lean_ctor_set_uint8(x_5, sizeof(void*)*2, x_3);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 1, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 2, x_3);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 3, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 4, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 5, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 6, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 7, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 8, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 9, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 10, x_3);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 11, x_3);
return x_5;
x_5 = 0;
x_6 = lean_alloc_ctor(0, 2, 12);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_2);
lean_ctor_set_uint8(x_6, sizeof(void*)*2, x_3);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 1, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 2, x_3);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 3, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 4, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 5, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 6, x_5);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 7, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 8, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 9, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 10, x_3);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 11, x_3);
return x_6;
}
}
static lean_object* _init_l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_mkProof_go___lambda__1___closed__2() {

1817
stage0/stdlib/Lean/Elab/Tactic/Simp.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -46783,26 +46783,27 @@ return x_5;
static lean_object* _init_l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__4() {
_start:
{
uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
uint8_t x_1; uint8_t x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_1 = 0;
x_2 = 1;
x_3 = 1;
x_4 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, 1, x_1);
lean_ctor_set_uint8(x_4, 2, x_1);
lean_ctor_set_uint8(x_4, 3, x_1);
lean_ctor_set_uint8(x_4, 4, x_1);
lean_ctor_set_uint8(x_4, 5, x_2);
lean_ctor_set_uint8(x_4, 6, x_3);
lean_ctor_set_uint8(x_4, 7, x_1);
lean_ctor_set_uint8(x_4, 8, x_3);
lean_ctor_set_uint8(x_4, 9, x_3);
lean_ctor_set_uint8(x_4, 10, x_1);
lean_ctor_set_uint8(x_4, 11, x_3);
lean_ctor_set_uint8(x_4, 12, x_3);
lean_ctor_set_uint8(x_4, 13, x_3);
return x_4;
x_4 = 0;
x_5 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_5, 0, x_1);
lean_ctor_set_uint8(x_5, 1, x_1);
lean_ctor_set_uint8(x_5, 2, x_1);
lean_ctor_set_uint8(x_5, 3, x_1);
lean_ctor_set_uint8(x_5, 4, x_1);
lean_ctor_set_uint8(x_5, 5, x_2);
lean_ctor_set_uint8(x_5, 6, x_3);
lean_ctor_set_uint8(x_5, 7, x_1);
lean_ctor_set_uint8(x_5, 8, x_3);
lean_ctor_set_uint8(x_5, 9, x_3);
lean_ctor_set_uint8(x_5, 10, x_1);
lean_ctor_set_uint8(x_5, 11, x_3);
lean_ctor_set_uint8(x_5, 12, x_3);
lean_ctor_set_uint8(x_5, 13, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___closed__5() {

195
stage0/stdlib/Lean/Meta/Basic.c generated
View file

@ -425,6 +425,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_getDefInfoTemp
LEAN_EXPORT lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_getLevelMVarDepth___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withNewBinderInfos(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_useEtaStruct(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withTransparency(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -801,7 +802,7 @@ static lean_object* l_Lean_Meta_processPostponed_loop___closed__4;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_approxDefEqImp(lean_object*);
lean_object* l_Lean_mkForall(lean_object*, uint8_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Meta_Basic___hyg_13645_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Meta_Basic___hyg_13722_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_instMonadMCtxMetaM___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_resettingSynthInstanceCacheWhen(lean_object*);
@ -1019,6 +1020,7 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_throwUnknownFVar___spe
LEAN_EXPORT lean_object* l_Lean_Meta_findLocalDecl_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Util_Trace_0__Lean_getResetTraces___at___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___spec__7___rarg___boxed(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_useEtaStruct___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_savingCacheImpl___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MetavarContext_hasAssignableMVar(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_getFVarLocalDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1165,7 +1167,7 @@ static uint8_t _init_l_Lean_Meta_Config_etaStruct___default() {
_start:
{
uint8_t x_1;
x_1 = 1;
x_1 = 0;
return x_1;
}
}
@ -2117,26 +2119,27 @@ return x_1;
static lean_object* _init_l_Lean_Meta_Context_config___default___closed__1() {
_start:
{
uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
uint8_t x_1; uint8_t x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_1 = 0;
x_2 = 1;
x_3 = 1;
x_4 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, 1, x_1);
lean_ctor_set_uint8(x_4, 2, x_1);
lean_ctor_set_uint8(x_4, 3, x_1);
lean_ctor_set_uint8(x_4, 4, x_1);
lean_ctor_set_uint8(x_4, 5, x_2);
lean_ctor_set_uint8(x_4, 6, x_3);
lean_ctor_set_uint8(x_4, 7, x_1);
lean_ctor_set_uint8(x_4, 8, x_3);
lean_ctor_set_uint8(x_4, 9, x_3);
lean_ctor_set_uint8(x_4, 10, x_1);
lean_ctor_set_uint8(x_4, 11, x_3);
lean_ctor_set_uint8(x_4, 12, x_3);
lean_ctor_set_uint8(x_4, 13, x_3);
return x_4;
x_4 = 0;
x_5 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_5, 0, x_1);
lean_ctor_set_uint8(x_5, 1, x_1);
lean_ctor_set_uint8(x_5, 2, x_1);
lean_ctor_set_uint8(x_5, 3, x_1);
lean_ctor_set_uint8(x_5, 4, x_1);
lean_ctor_set_uint8(x_5, 5, x_2);
lean_ctor_set_uint8(x_5, 6, x_3);
lean_ctor_set_uint8(x_5, 7, x_1);
lean_ctor_set_uint8(x_5, 8, x_3);
lean_ctor_set_uint8(x_5, 9, x_3);
lean_ctor_set_uint8(x_5, 10, x_1);
lean_ctor_set_uint8(x_5, 11, x_3);
lean_ctor_set_uint8(x_5, 12, x_3);
lean_ctor_set_uint8(x_5, 13, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_Meta_Context_config___default() {
@ -5501,6 +5504,156 @@ lean_dec(x_2);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_useEtaStruct(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_7 = l_Lean_Meta_getConfig(x_2, x_3, x_4, x_5, x_6);
x_8 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
x_9 = lean_ctor_get_uint8(x_8, 13);
lean_dec(x_8);
switch (x_9) {
case 0:
{
uint8_t x_10;
lean_dec(x_1);
x_10 = !lean_is_exclusive(x_7);
if (x_10 == 0)
{
lean_object* x_11; uint8_t x_12; lean_object* x_13;
x_11 = lean_ctor_get(x_7, 0);
lean_dec(x_11);
x_12 = 1;
x_13 = lean_box(x_12);
lean_ctor_set(x_7, 0, x_13);
return x_7;
}
else
{
lean_object* x_14; uint8_t x_15; lean_object* x_16; lean_object* x_17;
x_14 = lean_ctor_get(x_7, 1);
lean_inc(x_14);
lean_dec(x_7);
x_15 = 1;
x_16 = lean_box(x_15);
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_14);
return x_17;
}
}
case 1:
{
lean_object* x_18; lean_object* x_19; uint8_t x_20;
x_18 = lean_ctor_get(x_7, 1);
lean_inc(x_18);
lean_dec(x_7);
x_19 = lean_st_ref_get(x_5, x_18);
x_20 = !lean_is_exclusive(x_19);
if (x_20 == 0)
{
lean_object* x_21; lean_object* x_22; uint8_t x_23;
x_21 = lean_ctor_get(x_19, 0);
x_22 = lean_ctor_get(x_21, 0);
lean_inc(x_22);
lean_dec(x_21);
x_23 = lean_is_class(x_22, x_1);
if (x_23 == 0)
{
uint8_t x_24; lean_object* x_25;
x_24 = 1;
x_25 = lean_box(x_24);
lean_ctor_set(x_19, 0, x_25);
return x_19;
}
else
{
uint8_t x_26; lean_object* x_27;
x_26 = 0;
x_27 = lean_box(x_26);
lean_ctor_set(x_19, 0, x_27);
return x_19;
}
}
else
{
lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31;
x_28 = lean_ctor_get(x_19, 0);
x_29 = lean_ctor_get(x_19, 1);
lean_inc(x_29);
lean_inc(x_28);
lean_dec(x_19);
x_30 = lean_ctor_get(x_28, 0);
lean_inc(x_30);
lean_dec(x_28);
x_31 = lean_is_class(x_30, x_1);
if (x_31 == 0)
{
uint8_t x_32; lean_object* x_33; lean_object* x_34;
x_32 = 1;
x_33 = lean_box(x_32);
x_34 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_34, 0, x_33);
lean_ctor_set(x_34, 1, x_29);
return x_34;
}
else
{
uint8_t x_35; lean_object* x_36; lean_object* x_37;
x_35 = 0;
x_36 = lean_box(x_35);
x_37 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_37, 0, x_36);
lean_ctor_set(x_37, 1, x_29);
return x_37;
}
}
}
default:
{
uint8_t x_38;
lean_dec(x_1);
x_38 = !lean_is_exclusive(x_7);
if (x_38 == 0)
{
lean_object* x_39; uint8_t x_40; lean_object* x_41;
x_39 = lean_ctor_get(x_7, 0);
lean_dec(x_39);
x_40 = 0;
x_41 = lean_box(x_40);
lean_ctor_set(x_7, 0, x_41);
return x_7;
}
else
{
lean_object* x_42; uint8_t x_43; lean_object* x_44; lean_object* x_45;
x_42 = lean_ctor_get(x_7, 1);
lean_inc(x_42);
lean_dec(x_7);
x_43 = 0;
x_44 = lean_box(x_43);
x_45 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_45, 0, x_44);
lean_ctor_set(x_45, 1, x_42);
return x_45;
}
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_useEtaStruct___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_Lean_Meta_useEtaStruct(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_whnf___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
@ -42183,7 +42336,7 @@ lean_dec(x_3);
return x_9;
}
}
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Meta_Basic___hyg_13645_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Meta_Basic___hyg_13722_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -42668,7 +42821,7 @@ l_Lean_Meta_isExprDefEq___closed__1 = _init_l_Lean_Meta_isExprDefEq___closed__1(
lean_mark_persistent(l_Lean_Meta_isExprDefEq___closed__1);
l_Lean_Meta_isExprDefEq___closed__2 = _init_l_Lean_Meta_isExprDefEq___closed__2();
lean_mark_persistent(l_Lean_Meta_isExprDefEq___closed__2);
res = l_Lean_initFn____x40_Lean_Meta_Basic___hyg_13645_(lean_io_mk_world());
res = l_Lean_initFn____x40_Lean_Meta_Basic___hyg_13722_(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));

2975
stage0/stdlib/Lean/Meta/ExprDefEq.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -4026,26 +4026,27 @@ return x_19;
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_470____lambda__1___closed__1() {
_start:
{
uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
uint8_t x_1; uint8_t x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_1 = 0;
x_2 = 1;
x_3 = 1;
x_4 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, 1, x_1);
lean_ctor_set_uint8(x_4, 2, x_1);
lean_ctor_set_uint8(x_4, 3, x_1);
lean_ctor_set_uint8(x_4, 4, x_1);
lean_ctor_set_uint8(x_4, 5, x_2);
lean_ctor_set_uint8(x_4, 6, x_3);
lean_ctor_set_uint8(x_4, 7, x_1);
lean_ctor_set_uint8(x_4, 8, x_3);
lean_ctor_set_uint8(x_4, 9, x_3);
lean_ctor_set_uint8(x_4, 10, x_1);
lean_ctor_set_uint8(x_4, 11, x_3);
lean_ctor_set_uint8(x_4, 12, x_3);
lean_ctor_set_uint8(x_4, 13, x_3);
return x_4;
x_4 = 0;
x_5 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_5, 0, x_1);
lean_ctor_set_uint8(x_5, 1, x_1);
lean_ctor_set_uint8(x_5, 2, x_1);
lean_ctor_set_uint8(x_5, 3, x_1);
lean_ctor_set_uint8(x_5, 4, x_1);
lean_ctor_set_uint8(x_5, 5, x_2);
lean_ctor_set_uint8(x_5, 6, x_3);
lean_ctor_set_uint8(x_5, 7, x_1);
lean_ctor_set_uint8(x_5, 8, x_3);
lean_ctor_set_uint8(x_5, 9, x_3);
lean_ctor_set_uint8(x_5, 10, x_1);
lean_ctor_set_uint8(x_5, 11, x_3);
lean_ctor_set_uint8(x_5, 12, x_3);
lean_ctor_set_uint8(x_5, 13, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Instances___hyg_470____lambda__1___closed__2() {

6
stage0/stdlib/Lean/Meta/Match/MatchEqs.c generated
View file

@ -26508,7 +26508,7 @@ x_11 = !lean_is_exclusive(x_10);
if (x_11 == 0)
{
uint8_t x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_12 = 0;
x_12 = 2;
lean_ctor_set_uint8(x_10, 13, x_12);
x_13 = lean_st_ref_get(x_7, x_8);
x_14 = lean_ctor_get(x_13, 0);
@ -26697,7 +26697,7 @@ x_64 = lean_ctor_get_uint8(x_10, 10);
x_65 = lean_ctor_get_uint8(x_10, 11);
x_66 = lean_ctor_get_uint8(x_10, 12);
lean_dec(x_10);
x_67 = 0;
x_67 = 2;
x_68 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_68, 0, x_54);
lean_ctor_set_uint8(x_68, 1, x_55);
@ -26928,7 +26928,7 @@ if (lean_is_exclusive(x_110)) {
lean_dec_ref(x_110);
x_129 = lean_box(0);
}
x_130 = 0;
x_130 = 2;
if (lean_is_scalar(x_129)) {
x_131 = lean_alloc_ctor(0, 0, 14);
} else {

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

@ -9391,26 +9391,27 @@ return x_6;
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2697____lambda__2___closed__1() {
_start:
{
uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
uint8_t x_1; uint8_t x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_1 = 0;
x_2 = 1;
x_3 = 1;
x_4 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, 1, x_1);
lean_ctor_set_uint8(x_4, 2, x_1);
lean_ctor_set_uint8(x_4, 3, x_1);
lean_ctor_set_uint8(x_4, 4, x_1);
lean_ctor_set_uint8(x_4, 5, x_2);
lean_ctor_set_uint8(x_4, 6, x_3);
lean_ctor_set_uint8(x_4, 7, x_1);
lean_ctor_set_uint8(x_4, 8, x_3);
lean_ctor_set_uint8(x_4, 9, x_3);
lean_ctor_set_uint8(x_4, 10, x_1);
lean_ctor_set_uint8(x_4, 11, x_3);
lean_ctor_set_uint8(x_4, 12, x_3);
lean_ctor_set_uint8(x_4, 13, x_3);
return x_4;
x_4 = 0;
x_5 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_5, 0, x_1);
lean_ctor_set_uint8(x_5, 1, x_1);
lean_ctor_set_uint8(x_5, 2, x_1);
lean_ctor_set_uint8(x_5, 3, x_1);
lean_ctor_set_uint8(x_5, 4, x_1);
lean_ctor_set_uint8(x_5, 5, x_2);
lean_ctor_set_uint8(x_5, 6, x_3);
lean_ctor_set_uint8(x_5, 7, x_1);
lean_ctor_set_uint8(x_5, 8, x_3);
lean_ctor_set_uint8(x_5, 9, x_3);
lean_ctor_set_uint8(x_5, 10, x_1);
lean_ctor_set_uint8(x_5, 11, x_3);
lean_ctor_set_uint8(x_5, 12, x_3);
lean_ctor_set_uint8(x_5, 13, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2697____lambda__2___closed__2() {

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

File diff suppressed because it is too large Load diff

35
stage0/stdlib/Lean/Meta/Tactic/Acyclic.c generated
View file

@ -358,27 +358,28 @@ return x_1;
static lean_object* _init_l_Lean_Meta_acyclic_go___closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
lean_object* x_1; lean_object* x_2; uint8_t x_3; uint8_t x_4; uint8_t x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Simp_defaultMaxSteps;
x_2 = lean_unsigned_to_nat(2u);
x_3 = 0;
x_4 = 1;
x_5 = lean_alloc_ctor(0, 2, 12);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
lean_ctor_set_uint8(x_5, sizeof(void*)*2, x_3);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 1, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 2, x_3);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 3, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 4, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 5, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 6, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 7, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 8, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 9, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 10, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 11, x_3);
return x_5;
x_5 = 0;
x_6 = lean_alloc_ctor(0, 2, 12);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_2);
lean_ctor_set_uint8(x_6, sizeof(void*)*2, x_3);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 1, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 2, x_3);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 3, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 4, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 5, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 6, x_5);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 7, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 8, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 9, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 10, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 11, x_3);
return x_6;
}
}
static lean_object* _init_l_Lean_Meta_acyclic_go___closed__19() {

1900
stage0/stdlib/Lean/Meta/Tactic/Contradiction.c generated
View file

File diff suppressed because it is too large Load diff

35
stage0/stdlib/Lean/Meta/Tactic/Simp/SimpCongrTheorems.c generated
View file

@ -9877,26 +9877,27 @@ return x_10;
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1704____lambda__1___closed__1() {
_start:
{
uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
uint8_t x_1; uint8_t x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_1 = 0;
x_2 = 1;
x_3 = 1;
x_4 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, 1, x_1);
lean_ctor_set_uint8(x_4, 2, x_1);
lean_ctor_set_uint8(x_4, 3, x_1);
lean_ctor_set_uint8(x_4, 4, x_1);
lean_ctor_set_uint8(x_4, 5, x_2);
lean_ctor_set_uint8(x_4, 6, x_3);
lean_ctor_set_uint8(x_4, 7, x_1);
lean_ctor_set_uint8(x_4, 8, x_3);
lean_ctor_set_uint8(x_4, 9, x_3);
lean_ctor_set_uint8(x_4, 10, x_1);
lean_ctor_set_uint8(x_4, 11, x_3);
lean_ctor_set_uint8(x_4, 12, x_3);
lean_ctor_set_uint8(x_4, 13, x_3);
return x_4;
x_4 = 0;
x_5 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_5, 0, x_1);
lean_ctor_set_uint8(x_5, 1, x_1);
lean_ctor_set_uint8(x_5, 2, x_1);
lean_ctor_set_uint8(x_5, 3, x_1);
lean_ctor_set_uint8(x_5, 4, x_1);
lean_ctor_set_uint8(x_5, 5, x_2);
lean_ctor_set_uint8(x_5, 6, x_3);
lean_ctor_set_uint8(x_5, 7, x_1);
lean_ctor_set_uint8(x_5, 8, x_3);
lean_ctor_set_uint8(x_5, 9, x_3);
lean_ctor_set_uint8(x_5, 10, x_1);
lean_ctor_set_uint8(x_5, 11, x_3);
lean_ctor_set_uint8(x_5, 12, x_3);
lean_ctor_set_uint8(x_5, 13, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_Simp_SimpCongrTheorems___hyg_1704____lambda__1___closed__2() {

35
stage0/stdlib/Lean/Meta/Tactic/Simp/SimpTheorems.c generated
View file

@ -11326,26 +11326,27 @@ return x_25;
static lean_object* _init_l_Lean_Meta_mkSimpAttr___lambda__1___closed__1() {
_start:
{
uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
uint8_t x_1; uint8_t x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_1 = 0;
x_2 = 1;
x_3 = 1;
x_4 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, 1, x_1);
lean_ctor_set_uint8(x_4, 2, x_1);
lean_ctor_set_uint8(x_4, 3, x_1);
lean_ctor_set_uint8(x_4, 4, x_1);
lean_ctor_set_uint8(x_4, 5, x_2);
lean_ctor_set_uint8(x_4, 6, x_3);
lean_ctor_set_uint8(x_4, 7, x_1);
lean_ctor_set_uint8(x_4, 8, x_3);
lean_ctor_set_uint8(x_4, 9, x_3);
lean_ctor_set_uint8(x_4, 10, x_1);
lean_ctor_set_uint8(x_4, 11, x_3);
lean_ctor_set_uint8(x_4, 12, x_3);
lean_ctor_set_uint8(x_4, 13, x_3);
return x_4;
x_4 = 0;
x_5 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_5, 0, x_1);
lean_ctor_set_uint8(x_5, 1, x_1);
lean_ctor_set_uint8(x_5, 2, x_1);
lean_ctor_set_uint8(x_5, 3, x_1);
lean_ctor_set_uint8(x_5, 4, x_1);
lean_ctor_set_uint8(x_5, 5, x_2);
lean_ctor_set_uint8(x_5, 6, x_3);
lean_ctor_set_uint8(x_5, 7, x_1);
lean_ctor_set_uint8(x_5, 8, x_3);
lean_ctor_set_uint8(x_5, 9, x_3);
lean_ctor_set_uint8(x_5, 10, x_1);
lean_ctor_set_uint8(x_5, 11, x_3);
lean_ctor_set_uint8(x_5, 12, x_3);
lean_ctor_set_uint8(x_5, 13, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_Meta_mkSimpAttr___lambda__1___closed__2() {

70
stage0/stdlib/Lean/Meta/Tactic/Simp/Types.c generated
View file

@ -162,27 +162,28 @@ return x_1;
static lean_object* _init_l_Lean_Meta_Simp_Context_config___default___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
lean_object* x_1; lean_object* x_2; uint8_t x_3; uint8_t x_4; uint8_t x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Simp_defaultMaxSteps;
x_2 = lean_unsigned_to_nat(2u);
x_3 = 0;
x_4 = 1;
x_5 = lean_alloc_ctor(0, 2, 12);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
lean_ctor_set_uint8(x_5, sizeof(void*)*2, x_3);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 1, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 2, x_3);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 3, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 4, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 5, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 6, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 7, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 8, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 9, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 10, x_3);
lean_ctor_set_uint8(x_5, sizeof(void*)*2 + 11, x_3);
return x_5;
x_5 = 0;
x_6 = lean_alloc_ctor(0, 2, 12);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_2);
lean_ctor_set_uint8(x_6, sizeof(void*)*2, x_3);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 1, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 2, x_3);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 3, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 4, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 5, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 6, x_5);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 7, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 8, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 9, x_4);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 10, x_3);
lean_ctor_set_uint8(x_6, sizeof(void*)*2 + 11, x_3);
return x_6;
}
}
static lean_object* _init_l_Lean_Meta_Simp_Context_config___default() {
@ -290,25 +291,26 @@ return x_1;
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__1() {
_start:
{
lean_object* x_1; uint8_t x_2; lean_object* x_3;
lean_object* x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
x_1 = lean_unsigned_to_nat(0u);
x_2 = 0;
x_3 = lean_alloc_ctor(0, 2, 12);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*2, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 1, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 2, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 3, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 4, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 5, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 6, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 7, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 8, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 9, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 10, x_2);
lean_ctor_set_uint8(x_3, sizeof(void*)*2 + 11, x_2);
return x_3;
x_3 = 0;
x_4 = lean_alloc_ctor(0, 2, 12);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_1);
lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*2 + 1, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*2 + 2, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*2 + 3, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*2 + 4, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*2 + 5, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*2 + 6, x_3);
lean_ctor_set_uint8(x_4, sizeof(void*)*2 + 7, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*2 + 8, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*2 + 9, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*2 + 10, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*2 + 11, x_2);
return x_4;
}
}
static lean_object* _init_l_Lean_Meta_Simp_instInhabitedContext___closed__2() {

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

@ -4269,26 +4269,27 @@ return x_9;
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_723____lambda__1___closed__1() {
_start:
{
uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
uint8_t x_1; uint8_t x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_1 = 0;
x_2 = 1;
x_3 = 1;
x_4 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, 1, x_1);
lean_ctor_set_uint8(x_4, 2, x_1);
lean_ctor_set_uint8(x_4, 3, x_1);
lean_ctor_set_uint8(x_4, 4, x_1);
lean_ctor_set_uint8(x_4, 5, x_2);
lean_ctor_set_uint8(x_4, 6, x_3);
lean_ctor_set_uint8(x_4, 7, x_1);
lean_ctor_set_uint8(x_4, 8, x_3);
lean_ctor_set_uint8(x_4, 9, x_3);
lean_ctor_set_uint8(x_4, 10, x_1);
lean_ctor_set_uint8(x_4, 11, x_3);
lean_ctor_set_uint8(x_4, 12, x_3);
lean_ctor_set_uint8(x_4, 13, x_3);
return x_4;
x_4 = 0;
x_5 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_5, 0, x_1);
lean_ctor_set_uint8(x_5, 1, x_1);
lean_ctor_set_uint8(x_5, 2, x_1);
lean_ctor_set_uint8(x_5, 3, x_1);
lean_ctor_set_uint8(x_5, 4, x_1);
lean_ctor_set_uint8(x_5, 5, x_2);
lean_ctor_set_uint8(x_5, 6, x_3);
lean_ctor_set_uint8(x_5, 7, x_1);
lean_ctor_set_uint8(x_5, 8, x_3);
lean_ctor_set_uint8(x_5, 9, x_3);
lean_ctor_set_uint8(x_5, 10, x_1);
lean_ctor_set_uint8(x_5, 11, x_3);
lean_ctor_set_uint8(x_5, 12, x_3);
lean_ctor_set_uint8(x_5, 13, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_UnificationHint___hyg_723____lambda__1___closed__2() {

6
stage0/stdlib/Lean/Meta/WHNF.c generated
View file

@ -218,6 +218,7 @@ lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_reduceBinNatOp___closed__10;
static lean_object* l_Lean_Meta_reduceNat_x3f___closed__10;
lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_useEtaStruct(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_WHNF_0__Lean_Meta_cached_x3f___closed__2;
lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_reduceNat_x3f___closed__11;
@ -4741,10 +4742,11 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_WHNF_0__Lean_Meta_toCtorWhenStruc
_start:
{
lean_object* x_8; lean_object* x_9; uint8_t x_10;
x_8 = l_Lean_Meta_getConfig(x_3, x_4, x_5, x_6, x_7);
lean_inc(x_1);
x_8 = l_Lean_Meta_useEtaStruct(x_1, x_3, x_4, x_5, x_6, x_7);
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
x_10 = lean_ctor_get_uint8(x_9, 13);
x_10 = lean_unbox(x_9);
lean_dec(x_9);
if (x_10 == 0)
{

35
stage0/stdlib/Lean/ParserCompiler.c generated
View file

@ -30300,26 +30300,27 @@ return x_3;
static lean_object* _init_l_Lean_ParserCompiler_registerParserCompiler___rarg___lambda__1___closed__3() {
_start:
{
uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
uint8_t x_1; uint8_t x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_1 = 0;
x_2 = 1;
x_3 = 1;
x_4 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, 1, x_1);
lean_ctor_set_uint8(x_4, 2, x_1);
lean_ctor_set_uint8(x_4, 3, x_1);
lean_ctor_set_uint8(x_4, 4, x_1);
lean_ctor_set_uint8(x_4, 5, x_2);
lean_ctor_set_uint8(x_4, 6, x_3);
lean_ctor_set_uint8(x_4, 7, x_1);
lean_ctor_set_uint8(x_4, 8, x_3);
lean_ctor_set_uint8(x_4, 9, x_3);
lean_ctor_set_uint8(x_4, 10, x_1);
lean_ctor_set_uint8(x_4, 11, x_3);
lean_ctor_set_uint8(x_4, 12, x_3);
lean_ctor_set_uint8(x_4, 13, x_3);
return x_4;
x_4 = 0;
x_5 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_5, 0, x_1);
lean_ctor_set_uint8(x_5, 1, x_1);
lean_ctor_set_uint8(x_5, 2, x_1);
lean_ctor_set_uint8(x_5, 3, x_1);
lean_ctor_set_uint8(x_5, 4, x_1);
lean_ctor_set_uint8(x_5, 5, x_2);
lean_ctor_set_uint8(x_5, 6, x_3);
lean_ctor_set_uint8(x_5, 7, x_1);
lean_ctor_set_uint8(x_5, 8, x_3);
lean_ctor_set_uint8(x_5, 9, x_3);
lean_ctor_set_uint8(x_5, 10, x_1);
lean_ctor_set_uint8(x_5, 11, x_3);
lean_ctor_set_uint8(x_5, 12, x_3);
lean_ctor_set_uint8(x_5, 13, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_ParserCompiler_registerParserCompiler___rarg___lambda__1___closed__4() {

35
stage0/stdlib/Lean/PrettyPrinter.c generated
View file

@ -494,26 +494,27 @@ return x_4;
static lean_object* _init_l_Lean_PPContext_runMetaM___rarg___closed__1() {
_start:
{
uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
uint8_t x_1; uint8_t x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_1 = 0;
x_2 = 1;
x_3 = 1;
x_4 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, 1, x_1);
lean_ctor_set_uint8(x_4, 2, x_1);
lean_ctor_set_uint8(x_4, 3, x_1);
lean_ctor_set_uint8(x_4, 4, x_1);
lean_ctor_set_uint8(x_4, 5, x_2);
lean_ctor_set_uint8(x_4, 6, x_3);
lean_ctor_set_uint8(x_4, 7, x_1);
lean_ctor_set_uint8(x_4, 8, x_3);
lean_ctor_set_uint8(x_4, 9, x_3);
lean_ctor_set_uint8(x_4, 10, x_1);
lean_ctor_set_uint8(x_4, 11, x_3);
lean_ctor_set_uint8(x_4, 12, x_3);
lean_ctor_set_uint8(x_4, 13, x_3);
return x_4;
x_4 = 0;
x_5 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_5, 0, x_1);
lean_ctor_set_uint8(x_5, 1, x_1);
lean_ctor_set_uint8(x_5, 2, x_1);
lean_ctor_set_uint8(x_5, 3, x_1);
lean_ctor_set_uint8(x_5, 4, x_1);
lean_ctor_set_uint8(x_5, 5, x_2);
lean_ctor_set_uint8(x_5, 6, x_3);
lean_ctor_set_uint8(x_5, 7, x_1);
lean_ctor_set_uint8(x_5, 8, x_3);
lean_ctor_set_uint8(x_5, 9, x_3);
lean_ctor_set_uint8(x_5, 10, x_1);
lean_ctor_set_uint8(x_5, 11, x_3);
lean_ctor_set_uint8(x_5, 12, x_3);
lean_ctor_set_uint8(x_5, 13, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_PPContext_runMetaM___rarg___closed__2() {

35
stage0/stdlib/Lean/Server/Rpc/RequestHandling.c generated
View file

@ -5240,26 +5240,27 @@ return x_5;
static lean_object* _init_l_Lean_Server_registerRpcProcedure___lambda__2___closed__10() {
_start:
{
uint8_t x_1; uint8_t x_2; uint8_t x_3; lean_object* x_4;
uint8_t x_1; uint8_t x_2; uint8_t x_3; uint8_t x_4; lean_object* x_5;
x_1 = 0;
x_2 = 1;
x_3 = 1;
x_4 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_4, 0, x_1);
lean_ctor_set_uint8(x_4, 1, x_1);
lean_ctor_set_uint8(x_4, 2, x_1);
lean_ctor_set_uint8(x_4, 3, x_1);
lean_ctor_set_uint8(x_4, 4, x_1);
lean_ctor_set_uint8(x_4, 5, x_2);
lean_ctor_set_uint8(x_4, 6, x_3);
lean_ctor_set_uint8(x_4, 7, x_1);
lean_ctor_set_uint8(x_4, 8, x_3);
lean_ctor_set_uint8(x_4, 9, x_3);
lean_ctor_set_uint8(x_4, 10, x_1);
lean_ctor_set_uint8(x_4, 11, x_3);
lean_ctor_set_uint8(x_4, 12, x_3);
lean_ctor_set_uint8(x_4, 13, x_3);
return x_4;
x_4 = 0;
x_5 = lean_alloc_ctor(0, 0, 14);
lean_ctor_set_uint8(x_5, 0, x_1);
lean_ctor_set_uint8(x_5, 1, x_1);
lean_ctor_set_uint8(x_5, 2, x_1);
lean_ctor_set_uint8(x_5, 3, x_1);
lean_ctor_set_uint8(x_5, 4, x_1);
lean_ctor_set_uint8(x_5, 5, x_2);
lean_ctor_set_uint8(x_5, 6, x_3);
lean_ctor_set_uint8(x_5, 7, x_1);
lean_ctor_set_uint8(x_5, 8, x_3);
lean_ctor_set_uint8(x_5, 9, x_3);
lean_ctor_set_uint8(x_5, 10, x_1);
lean_ctor_set_uint8(x_5, 11, x_3);
lean_ctor_set_uint8(x_5, 12, x_3);
lean_ctor_set_uint8(x_5, 13, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_Server_registerRpcProcedure___lambda__2___closed__11() {