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-08-02 16:19:13 -07:00
parent 1ca62e21fd
commit bdc6bc6fcc
34 changed files with 7689 additions and 7040 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
stage0/src/Lean/Compiler/ConstFolding.lean generated
View file

@ -50,7 +50,7 @@ def getNumLit : Expr → Option Nat
| _ => none
def mkUIntLit (info : NumScalarTypeInfo) (n : Nat) : Expr :=
mkApp (mkConst info.ofNatFn) (mkNatLit (n%info.size))
mkApp (mkConst info.ofNatFn) (mkRawNatLit (n%info.size))
def mkUInt32Lit (n : Nat) : Expr :=
mkUIntLit {nbits := 32} n
@ -79,7 +79,7 @@ def foldNatBinOp (fn : Nat → Nat → Nat) (a₁ a₂ : Expr) : Option Expr :=
OptionM.run do
let n₁ ← getNumLit a₁
let n₂ ← getNumLit a₂
return mkNatLit (fn n₁ n₂)
return mkRawNatLit (fn n₁ n₂)
def foldNatAdd (_ : Bool) := foldNatBinOp Add.add
def foldNatMul (_ : Bool) := foldNatBinOp Mul.mul
@ -94,7 +94,7 @@ def foldNatPow (_ : Bool) (a₁ a₂ : Expr) : Option Expr :=
let n₁ ← getNumLit a₁
let n₂ ← getNumLit a₂
if n₂ < natPowThreshold then
return mkNatLit (n₁ ^ n₂)
return mkRawNatLit (n₁ ^ n₂)
else
failure
@ -168,7 +168,7 @@ def binFoldFns : List (Name × BinFoldFn) :=
def foldNatSucc (_ : Bool) (a : Expr) : Option Expr := OptionM.run do
let n ← getNumLit a
return mkNatLit (n+1)
return mkRawNatLit (n+1)
def foldCharOfNat (beforeErasure : Bool) (a : Expr) : Option Expr := OptionM.run do
guard (!beforeErasure)
@ -180,7 +180,7 @@ def foldCharOfNat (beforeErasure : Bool) (a : Expr) : Option Expr := OptionM.run
def foldToNat (_ : Bool) (a : Expr) : Option Expr := OptionM.run do
let n ← getNumLit a
return mkNatLit n
return mkRawNatLit n
def uintFoldToNatFns : List (Name × UnFoldFn) :=
numScalarTypes.foldl (fun r info => (info.toNatFn, foldToNat) :: r) []

9
stage0/src/Lean/Elab/BuiltinCommand.lean generated
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Elab.Command
import Lean.Elab.Open
namespace Lean.Elab.Command
@ -110,12 +111,8 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
let ids := stx[3].getArgs
let aliases ← ids.foldlM (init := []) fun (aliases : List (Name × Name)) (idStx : Syntax) => do
let id := idStx.getId
let declName := ns ++ id
if env.contains declName then
pure <| (currNamespace ++ id, declName) :: aliases
else
withRef idStx <| logUnknownDecl declName
pure aliases
let declName ← resolveOpenDeclId ns idStx
pure <| (currNamespace ++ id, declName) :: aliases
modify fun s => { s with env := aliases.foldl (init := s.env) fun env p => addAlias env p.1 p.2 }
@[builtinCommandElab «open»] def elabOpen : CommandElab := fun n => do

10
stage0/src/Lean/Elab/BuiltinTerm.lean generated
View file

@ -132,14 +132,14 @@ private def mkFreshTypeMVarFor (expectedType? : Option Expr) : TermElabM Expr :=
| none => throwIllFormedSyntax
let typeMVar ← mkFreshTypeMVarFor expectedType?
let u ← getDecLevel typeMVar
let mvar ← mkInstMVar (mkApp2 (Lean.mkConst ``OfNat [u]) typeMVar (mkNatLit val))
let r := mkApp3 (Lean.mkConst ``OfNat.ofNat [u]) typeMVar (mkNatLit val) mvar
let mvar ← mkInstMVar (mkApp2 (Lean.mkConst ``OfNat [u]) typeMVar (mkRawNatLit val))
let r := mkApp3 (Lean.mkConst ``OfNat.ofNat [u]) typeMVar (mkRawNatLit val) mvar
registerMVarErrorImplicitArgInfo mvar.mvarId! stx r
return r
@[builtinTermElab rawNatLit] def elabRawNatLit : TermElab := fun stx expectedType? => do
match stx[1].isNatLit? with
| some val => return mkNatLit val
| some val => return mkRawNatLit val
| none => throwIllFormedSyntax
@[builtinTermElab scientificLit]
@ -150,11 +150,11 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
let typeMVar ← mkFreshTypeMVarFor expectedType?
let u ← getDecLevel typeMVar
let mvar ← mkInstMVar (mkApp (Lean.mkConst ``OfScientific [u]) typeMVar)
return mkApp5 (Lean.mkConst ``OfScientific.ofScientific [u]) typeMVar mvar (mkNatLit m) (toExpr sign) (mkNatLit e)
return mkApp5 (Lean.mkConst ``OfScientific.ofScientific [u]) typeMVar mvar (mkRawNatLit m) (toExpr sign) (mkRawNatLit e)
@[builtinTermElab charLit] def elabCharLit : TermElab := fun stx _ => do
match stx.isCharLit? with
| some val => return mkApp (Lean.mkConst ``Char.ofNat) (mkNatLit val.toNat)
| some val => return mkApp (Lean.mkConst ``Char.ofNat) (mkRawNatLit val.toNat)
| none => throwIllFormedSyntax
@[builtinTermElab quotedName] def elabQuotedName : TermElab := fun stx _ =>

1
stage0/src/Lean/Elab/Command.lean generated
View file

@ -12,7 +12,6 @@ import Lean.Elab.Binders
import Lean.Elab.SyntheticMVars
import Lean.Elab.DeclModifiers
import Lean.Elab.InfoTree
import Lean.Elab.Open
import Lean.Elab.SetOption
namespace Lean.Elab.Command

39
stage0/src/Lean/Elab/Open.lean generated
View file

@ -22,6 +22,13 @@ instance : MonadResolveName (M (m := m)) where
getCurrNamespace := return (← get).currNamespace
getOpenDecls := return (← get).openDecls
def resolveId (ns : Name) (idStx : Syntax) : M (m := m) Name := do
let declName := ns ++ idStx.getId
if (← getEnv).contains declName then
return declName
else
withRef idStx <| resolveGlobalConstNoOverloadCore declName
private def addOpenDecl (decl : OpenDecl) : M (m:=m) Unit :=
modify fun s => { s with openDecls := decl :: s.openDecls }
@ -36,37 +43,27 @@ private def elabOpenSimple (n : Syntax) : M (m:=m) Unit :=
private def elabOpenOnly (n : Syntax) : M (m:=m) Unit := do
let ns ← resolveNamespace n[0].getId
for idStx in n[2].getArgs do
let id := idStx.getId
let declName := ns ++ id
if (← getEnv).contains declName then
addOpenDecl (OpenDecl.explicit id declName)
else
withRef idStx <| logUnknownDecl declName
let declName ← resolveId ns idStx
addOpenDecl (OpenDecl.explicit idStx.getId declName)
-- `open` id `hiding` id+
private def elabOpenHiding (n : Syntax) : M (m:=m) Unit := do
let ns ← resolveNamespace n[0].getId
let mut ids : List Name := []
for idStx in n[2].getArgs do
let declName ← resolveId ns idStx
let id := idStx.getId
let declName := ns ++ id
if (← getEnv).contains declName then
ids := id::ids
else
withRef idStx <| logUnknownDecl declName
ids := id::ids
addOpenDecl (OpenDecl.simple ns ids)
-- `open` id `renaming` sepBy (id `->` id) `,`
private def elabOpenRenaming (n : Syntax) : M (m:=m) Unit := do
let ns ← resolveNamespace n[0].getId
for stx in n[2].getSepArgs do
let fromId := stx[0].getId
let fromStx := stx[0]
let toId := stx[2].getId
let declName := ns ++ fromId
if (← getEnv).contains declName then
addOpenDecl (OpenDecl.explicit toId declName)
else
withRef stx do logUnknownDecl declName
let declName ← resolveId ns fromStx
addOpenDecl (OpenDecl.explicit toId declName)
def elabOpenDecl [MonadResolveName m] (openDeclStx : Syntax) : m (List OpenDecl) := do
StateRefT'.run' (s := { openDecls := (← getOpenDecls), currNamespace := (← getCurrNamespace) }) do
@ -80,8 +77,12 @@ def elabOpenDecl [MonadResolveName m] (openDeclStx : Syntax) : m (List OpenDecl)
elabOpenRenaming openDeclStx
return (← get).openDecls
def resolveOpenDeclId [MonadResolveName m] (ns : Name) (idStx : Syntax) : m Name := do
StateRefT'.run' (s := { openDecls := (← getOpenDecls), currNamespace := (← getCurrNamespace) }) do
OpenDecl.resolveId ns idStx
end OpenDecl
export OpenDecl (elabOpenDecl)
export OpenDecl (elabOpenDecl resolveOpenDeclId)
end Lean.Elab
end Lean.Elab

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

@ -58,7 +58,7 @@ structure StructView where
inductive StructFieldKind where
| newField | fromParent | subobject
deriving Inhabited
deriving Inhabited, BEq
structure StructFieldInfo where
name : Name
@ -470,6 +470,20 @@ private def addProjections (structName : Name) (projs : List ProjectionInfo) (is
| Except.ok env => setEnv env
| Except.error ex => throwKernelException ex
private def registerStructure (structName : Name) (infos : Array StructFieldInfo) : TermElabM Unit :=
modifyEnv fun env => Lean.registerStructure env {
structName
fields := infos.filterMap fun info =>
if info.kind == StructFieldKind.fromParent then
none
else
some {
fieldName := info.name
projFn := info.declName
subobject := info.kind == StructFieldKind.subobject
}
}
private def mkAuxConstructions (declName : Name) : TermElabM Unit := do
let env ← getEnv
let hasUnit := env.contains `PUnit
@ -530,6 +544,7 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
let projInfos := (fieldInfos.filter fun (info : StructFieldInfo) => !info.isFromParent).toList.map fun (info : StructFieldInfo) =>
{ declName := info.declName, inferMod := info.inferMod : ProjectionInfo }
addProjections view.declName projInfos view.isClass
registerStructure view.declName fieldInfos
mkAuxConstructions view.declName
let instParents ← fieldInfos.filterM fun info => do
let decl ← Term.getFVarLocalDecl! info.fvar

44
stage0/src/Lean/Expr.lean generated
View file

@ -236,15 +236,6 @@ def binderInfo (e : Expr) : BinderInfo :=
end Expr
def mkLit (l : Literal) : Expr :=
Expr.lit l $ mkData (mixHash 3 (hash l))
def mkNatLit (n : Nat) : Expr :=
mkLit (Literal.natVal n)
def mkStrLit (s : String) : Expr :=
mkLit (Literal.strVal s)
def mkConst (n : Name) (lvls : List Level := []) : Expr :=
Expr.const n lvls $ mkData (mixHash 5 $ mixHash (hash n) (hash lvls)) 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam)
@ -320,6 +311,30 @@ def mkLet (x : Name) (t : Expr) (v : Expr) (b : Expr) (nonDep : Bool := false) :
(t.hasLevelParam || v.hasLevelParam || b.hasLevelParam)
nonDep
def mkAppB (f a b : Expr) := mkApp (mkApp f a) b
def mkApp2 (f a b : Expr) := mkAppB f a b
def mkApp3 (f a b c : Expr) := mkApp (mkAppB f a b) c
def mkApp4 (f a b c d : Expr) := mkAppB (mkAppB f a b) c d
def mkApp5 (f a b c d e : Expr) := mkApp (mkApp4 f a b c d) e
def mkApp6 (f a b c d e₁ e₂ : Expr) := mkAppB (mkApp4 f a b c d) e₁ e₂
def mkApp7 (f a b c d e₁ e₂ e₃ : Expr) := mkApp3 (mkApp4 f a b c d) e₁ e₂ e₃
def mkApp8 (f a b c d e₁ e₂ e₃ e₄ : Expr) := mkApp4 (mkApp4 f a b c d) e₁ e₂ e₃ e₄
def mkApp9 (f a b c d e₁ e₂ e₃ e₄ e₅ : Expr) := mkApp5 (mkApp4 f a b c d) e₁ e₂ e₃ e₄ e₅
def mkApp10 (f a b c d e₁ e₂ e₃ e₄ e₅ e₆ : Expr) := mkApp6 (mkApp4 f a b c d) e₁ e₂ e₃ e₄ e₅ e₆
def mkLit (l : Literal) : Expr :=
Expr.lit l $ mkData (mixHash 3 (hash l))
def mkRawNatLit (n : Nat) : Expr :=
mkLit (Literal.natVal n)
def mkNatLit (n : Nat) : Expr :=
let r := mkRawNatLit n
mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst ``Nat) r (mkApp (mkConst ``instOfNatNat) r)
def mkStrLit (s : String) : Expr :=
mkLit (Literal.strVal s)
@[export lean_expr_mk_bvar] def mkBVarEx : Nat → Expr := mkBVar
@[export lean_expr_mk_fvar] def mkFVarEx : FVarId → Expr := mkFVar
@[export lean_expr_mk_mvar] def mkMVarEx : MVarId → Expr := mkMVar
@ -678,17 +693,6 @@ def isAtomic : Expr → Bool
end Expr
def mkAppB (f a b : Expr) := mkApp (mkApp f a) b
def mkApp2 (f a b : Expr) := mkAppB f a b
def mkApp3 (f a b c : Expr) := mkApp (mkAppB f a b) c
def mkApp4 (f a b c d : Expr) := mkAppB (mkAppB f a b) c d
def mkApp5 (f a b c d e : Expr) := mkApp (mkApp4 f a b c d) e
def mkApp6 (f a b c d e₁ e₂ : Expr) := mkAppB (mkApp4 f a b c d) e₁ e₂
def mkApp7 (f a b c d e₁ e₂ e₃ : Expr) := mkApp3 (mkApp4 f a b c d) e₁ e₂ e₃
def mkApp8 (f a b c d e₁ e₂ e₃ e₄ : Expr) := mkApp4 (mkApp4 f a b c d) e₁ e₂ e₃ e₄
def mkApp9 (f a b c d e₁ e₂ e₃ e₄ e₅ : Expr) := mkApp5 (mkApp4 f a b c d) e₁ e₂ e₃ e₄ e₅
def mkApp10 (f a b c d e₁ e₂ e₃ e₄ e₅ e₆ : Expr) := mkApp6 (mkApp4 f a b c d) e₁ e₂ e₃ e₄ e₅ e₆
def mkDecIsTrue (pred proof : Expr) :=
mkAppB (mkConst `Decidable.isTrue) pred proof

4
stage0/src/Lean/Meta/AppBuilder.lean generated
View file

@ -482,8 +482,8 @@ def isMonad? (m : Expr) : MetaM (Option Expr) :=
/-- Return `(n : type)`, a numeric literal of type `type`. The method fails if we don't have an instance `OfNat type n` -/
def mkNumeral (type : Expr) (n : Nat) : MetaM Expr := do
let u ← getDecLevel type
let inst ← synthInstance (mkApp2 (mkConst ``OfNat [u]) type (mkNatLit n))
return mkApp3 (mkConst ``OfNat.ofNat [u]) type (mkNatLit n) inst
let inst ← synthInstance (mkApp2 (mkConst ``OfNat [u]) type (mkRawNatLit n))
return mkApp3 (mkConst ``OfNat.ofNat [u]) type (mkRawNatLit n) inst
/--
Return `a op b`, where `op` has name `opName` and is implemented using the typeclass `className`.

8
stage0/src/Lean/Meta/Match/CaseArraySizes.lean generated
View file

@ -25,9 +25,9 @@ def getArrayArgType (a : Expr) : MetaM Expr := do
pure aType.appArg!
private def mkArrayGetLit (a : Expr) (i : Nat) (n : Nat) (h : Expr) : MetaM Expr := do
let lt ← mkLt (mkNatLit i) (mkNatLit n)
let lt ← mkLt (mkRawNatLit i) (mkRawNatLit n)
let ltPrf ← mkDecideProof lt
mkAppM `Array.getLit #[a, mkNatLit i, h, ltPrf]
mkAppM `Array.getLit #[a, mkRawNatLit i, h, ltPrf]
private partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNamePrefix : Name) (aSizeEqN : Expr) : MetaM MVarId := do
let α ← getArrayArgType a
@ -41,7 +41,7 @@ private partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNameP
else
let xsLit ← mkArrayLit α xs.toList
let aEqXsLit ← mkEq a xsLit
let aEqLitPrf ← mkAppM `Array.toArrayLitEq #[a, mkNatLit n, aSizeEqN]
let aEqLitPrf ← mkAppM `Array.toArrayLitEq #[a, mkRawNatLit n, aSizeEqN]
withLocalDeclD `hEqALit aEqXsLit fun heq => do
let target ← getMVarType mvarId
let newTarget ← mkForallFVars (xs.push heq) target
@ -67,7 +67,7 @@ def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNam
let mvarId ← assertExt mvarId `aSize (mkConst `Nat) aSize
let (aSizeFVarId, mvarId) ← intro1 mvarId
let (hEq, mvarId) ← intro1 mvarId
let subgoals ← caseValues mvarId aSizeFVarId (sizes.map mkNatLit) hNamePrefix
let subgoals ← caseValues mvarId aSizeFVarId (sizes.map mkRawNatLit) hNamePrefix
subgoals.mapIdxM fun i subgoal => do
let subst := subgoal.subst
let mvarId := subgoal.mvarId

18
stage0/src/Lean/Meta/Match/Match.lean generated
View file

@ -538,7 +538,7 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
private def expandNatValuePattern (p : Problem) : Problem := do
let alts := p.alts.map fun alt => match alt.patterns with
| Pattern.val (Expr.lit (Literal.natVal 0) _) :: ps => { alt with patterns := Pattern.ctor `Nat.zero [] [] [] :: ps }
| Pattern.val (Expr.lit (Literal.natVal (n+1)) _) :: ps => { alt with patterns := Pattern.ctor `Nat.succ [] [] [Pattern.val (mkNatLit n)] :: ps }
| Pattern.val (Expr.lit (Literal.natVal (n+1)) _) :: ps => { alt with patterns := Pattern.ctor `Nat.succ [] [] [Pattern.val (mkRawNatLit n)] :: ps }
| _ => alt
{ p with alts := alts }
@ -808,21 +808,21 @@ def getMkMatcherInputInContext (matcherApp : MatcherApp) : MetaM MkMatcherInput
let matcherName := matcherApp.matcherName
let some matcherInfo ← getMatcherInfo? matcherName | throwError "not a matcher: {matcherName}"
let matcherConst ← getConstInfo matcherName
let matcherType ← instantiateForall matcherConst.type $ matcherApp.params ++ #[matcherApp.motive]
let matcherType ← instantiateForall matcherConst.type $ matcherApp.params ++ #[matcherApp.motive]
let matchType ← do
let u :=
if let some idx := matcherInfo.uElimPos?
let u :=
if let some idx := matcherInfo.uElimPos?
then mkLevelParam matcherConst.levelParams.toArray[idx]
else levelZero
forallBoundedTelescope matcherType (some matcherInfo.numDiscrs) fun discrs t => do
mkForallFVars discrs (mkConst ``PUnit [u])
let matcherType ← instantiateForall matcherType matcherApp.discrs
let lhss := Array.toList $ ←forallBoundedTelescope matcherType (some matcherApp.alts.size) fun alts _ =>
let matcherType ← instantiateForall matcherType matcherApp.discrs
let lhss := Array.toList $ ←forallBoundedTelescope matcherType (some matcherApp.alts.size) fun alts _ =>
alts.mapM fun alt => do
let ty ← inferType alt
forallTelescope ty fun xs body => do
forallTelescope ty fun xs body => do
let xs ← xs.filterM fun x => dependsOn body x.fvarId!
body.withApp fun f args => do
let ctx ← getLCtx
@ -836,7 +836,7 @@ def getMkMatcherInputInContext (matcherApp : MatcherApp) : MetaM MkMatcherInput
return { matcherName, matchType, numDiscrs := matcherApp.discrs.size, lhss }
def withMkMatcherInput
def withMkMatcherInput
(matcherName : Name)
(k : MkMatcherInput → MetaM α) : MetaM α := do
let some matcherInfo ← getMatcherInfo? matcherName | throwError "not a matcher: {matcherName}"

4
stage0/src/Lean/Meta/Offset.lean generated
View file

@ -159,7 +159,7 @@ def isDefEqOffset (s t : Expr) : MetaM LBool := do
match (← evalNat t) with
| some v₂ => -- s+k₁ =?= v₂
if v₂ ≥ k₁ then
isDefEq s (mkNatLit $ v₂ - k₁)
isDefEq s (mkNatLit <| v₂ - k₁)
else
ifNatExpr <| return LBool.false
| none =>
@ -170,7 +170,7 @@ def isDefEqOffset (s t : Expr) : MetaM LBool := do
match (← isOffset t) with
| some (t, k₂) => -- v₁ =?= t+k₂
if v₁ ≥ k₂ then
isDefEq (mkNatLit $ v₁ - k₂) t
isDefEq (mkNatLit <| v₁ - k₂) t
else
ifNatExpr <| return LBool.false
| none =>

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

@ -60,7 +60,7 @@ private def mkNullaryCtor (type : Expr) (nparams : Nat) : MetaM (Option Expr) :=
def toCtorIfLit : Expr → Expr
| Expr.lit (Literal.natVal v) _ =>
if v == 0 then mkConst `Nat.zero
else mkApp (mkConst `Nat.succ) (mkNatLit (v-1))
else mkApp (mkConst `Nat.succ) (mkRawNatLit (v-1))
| Expr.lit (Literal.strVal v) _ =>
mkApp (mkConst `String.mk) (toExpr v.toList)
| e => e
@ -515,13 +515,13 @@ def reduceNative? (e : Expr) : MetaM (Option Expr) :=
def reduceUnaryNatOp (f : Nat → Nat) (a : Expr) : MetaM (Option Expr) :=
withNatValue a fun a =>
return mkNatLit <| f a
return mkRawNatLit <| f a
def reduceBinNatOp (f : Nat → Nat → Nat) (a b : Expr) : MetaM (Option Expr) :=
withNatValue a fun a =>
withNatValue b fun b => do
trace[Meta.isDefEq.whnf.reduceBinOp] "{a} op {b}"
return mkNatLit <| f a b
return mkRawNatLit <| f a b
def reduceBinNatPred (f : Nat → Nat → Bool) (a b : Expr) : MetaM (Option Expr) := do
withNatValue a fun a =>

2
stage0/src/Lean/Parser/Extension.lean generated
View file

@ -421,7 +421,7 @@ def runParserCategory (env : Environment) (catName : Name) (input : String) (fil
def declareBuiltinParser (env : Environment) (addFnName : Name) (catName : Name) (declName : Name) (prio : Nat) : IO Environment :=
let name := `_regBuiltinParser ++ declName
let type := mkApp (mkConst `IO) (mkConst `Unit)
let val := mkAppN (mkConst addFnName) #[toExpr catName, toExpr declName, mkConst declName, mkNatLit prio]
let val := mkAppN (mkConst addFnName) #[toExpr catName, toExpr declName, mkConst declName, mkRawNatLit prio]
let decl := Declaration.defnDecl { name := name, levelParams := [], type := type, value := val, hints := ReducibilityHints.opaque,
safety := DefinitionSafety.safe }
match env.addAndCompile {} decl with

38
stage0/src/Lean/Structure.lean generated
View file

@ -15,6 +15,42 @@ import Lean.ProjFns
namespace Lean
structure StructureFieldInfo where
fieldName : Name
projFn : Name
subobject : Bool
deriving Inhabited
private structure StructureEntry where
structName : Name
fieldNames : Array Name -- sorted by field position in the structure
fieldInfo : Array StructureFieldInfo -- sorted by `fieldName`
deriving Inhabited
/-- Auxiliary state for structures defined in the current module. -/
private structure StructureState where
map : Std.PersistentHashMap Name StructureEntry := {}
deriving Inhabited
builtin_initialize structureExt : SimplePersistentEnvExtension StructureEntry StructureState ← registerSimplePersistentEnvExtension {
name := `structExt
addImportedFn := fun _ => {}
addEntryFn := fun s e => { s with map := s.map.insert e.structName e }
toArrayFn := fun es => es.toArray.qsort fun e₁ e₂ => Name.quickLt e₁.structName e₂.structName
}
structure StructureDescr where
structName : Name
fields : Array StructureFieldInfo -- Should use the order the field appear in the constructor.
deriving Inhabited
def registerStructure (env : Environment) (e : StructureDescr) : Environment :=
structureExt.addEntry env {
structName := e.structName
fieldNames := e.fields.map fun e => e.fieldName
fieldInfo := e.fields.qsort fun e₁ e₂ => Name.quickLt e₁.fieldName e₂.fieldName
}
/--
Return true iff `constName` is the a non-recursive inductive
datatype that has only one constructor. -/
@ -52,6 +88,8 @@ private def getStructureFieldsAux (numParams : Nat) : Nat → Expr → Array Nam
| _, _, fieldNames => fieldNames
-- TODO: fix. See comment in the beginning of the file
/-- Get direct field names for the given structure. -/
def getStructureFields (env : Environment) (structName : Name) : Array Name :=
let ctor := getStructureCtor env structName;
getStructureFieldsAux ctor.numParams 0 ctor.type #[]

20
stage0/stdlib/Lean/Compiler/ConstFolding.c generated
View file

@ -148,6 +148,7 @@ lean_object* l_Lean_Compiler_foldNatDecLt(uint8_t, lean_object*, lean_object*);
uint8_t l_Lean_Compiler_isOfNat(lean_object*);
lean_object* l_Lean_Compiler_foldStrictOr___boxed(lean_object*);
static lean_object* l_Lean_Compiler_mkNatLt___closed__5;
lean_object* l_Lean_mkRawNatLit(lean_object*);
lean_object* l_Lean_Compiler_foldNatSucc___boxed(lean_object*);
static lean_object* l_Lean_Compiler_mkNatLe___closed__5;
static lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__8;
@ -315,7 +316,6 @@ lean_object* l_Lean_Compiler_foldBinOp_match__1(lean_object*);
lean_object* l_List_foldr___at_Lean_Compiler_isOfNat___spec__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_mkNatLe___closed__7;
lean_object* lean_nat_mod(lean_object*, lean_object*);
lean_object* l_Lean_mkNatLit(lean_object*);
static lean_object* l_Lean_Compiler_numScalarTypes___closed__7;
static lean_object* l_Lean_Compiler_natFoldFns___closed__1;
static lean_object* l_Lean_Compiler_numScalarTypes___closed__19;
@ -1231,7 +1231,7 @@ lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_nat_mod(x_2, x_6);
lean_dec(x_6);
x_8 = l_Lean_mkNatLit(x_7);
x_8 = l_Lean_mkRawNatLit(x_7);
x_9 = l_Lean_mkApp(x_5, x_8);
return x_9;
}
@ -2059,7 +2059,7 @@ if (x_9 == 0)
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = lean_ctor_get(x_7, 0);
x_11 = lean_apply_2(x_1, x_6, x_10);
x_12 = l_Lean_mkNatLit(x_11);
x_12 = l_Lean_mkRawNatLit(x_11);
lean_ctor_set(x_7, 0, x_12);
return x_7;
}
@ -2070,7 +2070,7 @@ x_13 = lean_ctor_get(x_7, 0);
lean_inc(x_13);
lean_dec(x_7);
x_14 = lean_apply_2(x_1, x_6, x_13);
x_15 = l_Lean_mkNatLit(x_14);
x_15 = l_Lean_mkRawNatLit(x_14);
x_16 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_16, 0, x_15);
return x_16;
@ -2278,7 +2278,7 @@ lean_object* x_13; lean_object* x_14;
x_13 = lean_nat_pow(x_5, x_9);
lean_dec(x_9);
lean_dec(x_5);
x_14 = l_Lean_mkNatLit(x_13);
x_14 = l_Lean_mkRawNatLit(x_13);
lean_ctor_set(x_6, 0, x_14);
return x_6;
}
@ -2305,7 +2305,7 @@ lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_nat_pow(x_5, x_15);
lean_dec(x_15);
lean_dec(x_5);
x_20 = l_Lean_mkNatLit(x_19);
x_20 = l_Lean_mkRawNatLit(x_19);
x_21 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_21, 0, x_20);
return x_21;
@ -4428,7 +4428,7 @@ x_5 = lean_ctor_get(x_2, 0);
x_6 = lean_unsigned_to_nat(1u);
x_7 = lean_nat_add(x_5, x_6);
lean_dec(x_5);
x_8 = l_Lean_mkNatLit(x_7);
x_8 = l_Lean_mkRawNatLit(x_7);
lean_ctor_set(x_2, 0, x_8);
return x_2;
}
@ -4441,7 +4441,7 @@ lean_dec(x_2);
x_10 = lean_unsigned_to_nat(1u);
x_11 = lean_nat_add(x_9, x_10);
lean_dec(x_9);
x_12 = l_Lean_mkNatLit(x_11);
x_12 = l_Lean_mkRawNatLit(x_11);
x_13 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_13, 0, x_12);
return x_13;
@ -4649,7 +4649,7 @@ if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_ctor_get(x_2, 0);
x_6 = l_Lean_mkNatLit(x_5);
x_6 = l_Lean_mkRawNatLit(x_5);
lean_ctor_set(x_2, 0, x_6);
return x_2;
}
@ -4659,7 +4659,7 @@ lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_2, 0);
lean_inc(x_7);
lean_dec(x_2);
x_8 = l_Lean_mkNatLit(x_7);
x_8 = l_Lean_mkRawNatLit(x_7);
x_9 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_9, 0, x_8);
return x_9;

3114
stage0/stdlib/Lean/Elab/BuiltinCommand.c generated
View file

File diff suppressed because it is too large Load diff

2232
stage0/stdlib/Lean/Elab/BuiltinTerm.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Elab.Command
// Imports: Init Lean.Parser.Command Lean.ResolveName Lean.Meta.Reduce Lean.Elab.Log Lean.Elab.Term Lean.Elab.Binders Lean.Elab.SyntheticMVars Lean.Elab.DeclModifiers Lean.Elab.InfoTree Lean.Elab.Open Lean.Elab.SetOption
// Imports: Init Lean.Parser.Command Lean.ResolveName Lean.Meta.Reduce Lean.Elab.Log Lean.Elab.Term Lean.Elab.Binders Lean.Elab.SyntheticMVars Lean.Elab.DeclModifiers Lean.Elab.InfoTree Lean.Elab.SetOption
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -18993,7 +18993,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Elab_Command_modifyScope___closed__1;
x_2 = l_Lean_Elab_Command_modifyScope___closed__2;
x_3 = lean_unsigned_to_nat(406u);
x_3 = lean_unsigned_to_nat(405u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_Elab_Command_modifyScope___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -21176,7 +21176,6 @@ lean_object* initialize_Lean_Elab_Binders(lean_object*);
lean_object* initialize_Lean_Elab_SyntheticMVars(lean_object*);
lean_object* initialize_Lean_Elab_DeclModifiers(lean_object*);
lean_object* initialize_Lean_Elab_InfoTree(lean_object*);
lean_object* initialize_Lean_Elab_Open(lean_object*);
lean_object* initialize_Lean_Elab_SetOption(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Elab_Command(lean_object* w) {
@ -21213,9 +21212,6 @@ lean_dec_ref(res);
res = initialize_Lean_Elab_InfoTree(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_Open(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_SetOption(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

3337
stage0/stdlib/Lean/Elab/Open.c generated
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

2317
stage0/stdlib/Lean/Elab/Tactic/BuiltinTactic.c generated
View file

File diff suppressed because it is too large Load diff

452
stage0/stdlib/Lean/Expr.c generated
View file

@ -18,6 +18,7 @@ lean_object* l_Lean_Expr_isBinding___boxed(lean_object*);
static lean_object* l_Lean_Expr_letName_x21___closed__2;
lean_object* l_Lean_Expr_data_match__1(lean_object*);
static lean_object* l_Lean_Expr_ctorName___closed__7;
static lean_object* l_Lean_mkNatLit___closed__8;
lean_object* l_Lean_instLTLiteral;
lean_object* l___private_Lean_Expr_0__Lean_beqBinderInfo____x40_Lean_Expr___hyg_312__match__1___rarg(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_bindingInfo_x21(lean_object*);
@ -32,6 +33,7 @@ lean_object* l_Lean_Expr_Data_hash___boxed(lean_object*);
lean_object* l_Lean_Expr_isApp_match__1___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__1;
lean_object* l_Lean_Expr_hasAnyFVar_visit_match__1(lean_object*);
static lean_object* l_Lean_mkNatLit___closed__4;
lean_object* l_Lean_Expr_mvarId_x21(lean_object*);
lean_object* l_Lean_Expr_bindingDomain_x21___boxed(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_reprLiteral____x40_Lean_Expr___hyg_98____closed__2;
@ -54,6 +56,7 @@ uint8_t l_UInt64_decEq(uint64_t, uint64_t);
static lean_object* l_Lean_Expr_bindingDomain_x21___closed__2;
lean_object* l_Lean_Expr_abstract___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Expr_getRevArg_x21___closed__1;
static lean_object* l_Lean_mkNatLit___closed__1;
lean_object* l_Lean_Expr_isAtomic_match__1(lean_object*);
lean_object* l_Lean_Expr_updateConst___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_mkDecIsTrue___closed__3;
@ -96,6 +99,7 @@ lean_object* l_Lean_ExprStructEq_instHashableExprStructEq;
lean_object* l___private_Lean_Expr_0__Lean_beqBinderInfo____x40_Lean_Expr___hyg_312__match__1(lean_object*);
uint64_t l_Bool_toUInt64(uint8_t);
static lean_object* l_Lean_Expr_updateMData_x21___closed__2;
static lean_object* l_Lean_mkNatLit___closed__9;
lean_object* l_Lean_Expr_instantiateLevelParamsArray___boxed(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isArrow(lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_Expr_betaRevAux(lean_object*, lean_object*, lean_object*, lean_object*);
@ -186,6 +190,7 @@ lean_object* l_Lean_Expr_getRevArgD(lean_object*, lean_object*, lean_object*);
uint64_t l_List_foldl___at_Lean_mkConst___spec__1(uint64_t, lean_object*);
lean_object* l_Lean_Expr_bindingName_x21_match__1(lean_object*);
static lean_object* l_Lean_Expr_getAppArgs___closed__1;
static lean_object* l_Lean_mkNatLit___closed__2;
uint8_t l_Lean_Level_hasParam(lean_object*);
lean_object* l_Lean_Expr_updateApp_x21(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_mkAppRevRange(lean_object*, lean_object*, lean_object*, lean_object*);
@ -294,6 +299,8 @@ lean_object* l_Lean_Expr_getRevArg_x21_match__1(lean_object*);
lean_object* l_Lean_Expr_isConstOf_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isLambda_match__1(lean_object*);
uint8_t lean_expr_has_mvar(lean_object*);
lean_object* l_Lean_mkRawNatLit(lean_object*);
static lean_object* l_Lean_mkNatLit___closed__6;
uint8_t l_Lean_KVMap_getBool(lean_object*, lean_object*, uint8_t);
static lean_object* l_Lean_Expr_ctorName___closed__5;
lean_object* l___private_Lean_Expr_0__Lean_Expr_mkAppRevRangeAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -464,6 +471,7 @@ lean_object* l___private_Lean_Expr_0__Lean_Expr_betaRevAux___boxed(lean_object*,
static lean_object* l_Lean_Expr_ctorName___closed__9;
lean_object* l_Lean_Expr_instantiateRevRange___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_hasLooseBVarInExplicitDomain_match__1___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
static lean_object* l_Lean_mkNatLit___closed__7;
uint8_t l_Lean_instInhabitedBinderInfo;
static lean_object* l_Lean_Expr_updateLambda_x21___closed__1;
lean_object* l_Lean_mkAppN___boxed(lean_object*, lean_object*);
@ -471,6 +479,7 @@ lean_object* l_Lean_Expr_mkDataForLet___boxed__const__1;
static lean_object* l_Lean_Expr_updateProj_x21___closed__1;
lean_object* lean_level_update_imax(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4;
static lean_object* l_Lean_mkNatLit___closed__3;
lean_object* l_Lean_ExprStructEq_beq_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isProj___boxed(lean_object*);
static lean_object* l_Lean_Expr_updateLambda_x21___closed__2;
@ -532,6 +541,7 @@ lean_object* l_Lean_BinderInfo_isImplicit_match__1(lean_object*);
lean_object* l_Lean_Expr_mkDataForBinder___boxed__const__1;
static lean_object* l_Lean_Expr_bvarIdx_x21___closed__1;
lean_object* lean_panic_fn(lean_object*, lean_object*);
static lean_object* l_Lean_mkNatLit___closed__10;
lean_object* l_Lean_Expr_withApp___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Expr_isAppOfArity___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_appArg_x21___boxed(lean_object*);
@ -551,6 +561,7 @@ lean_object* lean_expr_mk_proj(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isMVar_match__1(lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppRevArgsAux_match__1(lean_object*);
static lean_object* l_Lean_Expr_appFn_x21___closed__2;
static lean_object* l_Lean_mkNatLit___closed__5;
lean_object* l_Lean_Expr_Data_hasExprMVar___boxed(lean_object*);
static lean_object* l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__5;
lean_object* l_Lean_Expr_etaExpanded_x3f(lean_object*);
@ -690,7 +701,6 @@ lean_object* l_List_map___at_Lean_Expr_instantiateLevelParams___spec__4___boxed(
lean_object* l_Lean_mkAppB(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkApp10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isApp___boxed(lean_object*);
static lean_object* l_Lean_Expr_isCharLit___closed__4;
lean_object* l_Lean_mkApp8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkBVar(lean_object*);
uint8_t l_Lean_Expr_hasFVar(lean_object*);
@ -4121,42 +4131,6 @@ x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* l_Lean_mkLit(lean_object* x_1) {
_start:
{
uint64_t x_2; uint64_t x_3; uint64_t x_4; lean_object* x_5; uint8_t x_6; uint64_t x_7; lean_object* x_8;
x_2 = 3;
x_3 = l_Lean_Literal_hash(x_1);
x_4 = lean_uint64_mix_hash(x_2, x_3);
x_5 = lean_unsigned_to_nat(0u);
x_6 = 0;
x_7 = l_Lean_Expr_mkData(x_4, x_5, x_6, x_6, x_6, x_6);
x_8 = lean_alloc_ctor(9, 1, 8);
lean_ctor_set(x_8, 0, x_1);
lean_ctor_set_uint64(x_8, sizeof(void*)*1, x_7);
return x_8;
}
}
lean_object* l_Lean_mkNatLit(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
x_3 = l_Lean_mkLit(x_2);
return x_3;
}
}
lean_object* l_Lean_mkStrLit(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
x_3 = l_Lean_mkLit(x_2);
return x_3;
}
}
uint64_t l_List_foldl___at_Lean_mkConst___spec__1(uint64_t x_1, lean_object* x_2) {
_start:
{
@ -5813,6 +5787,241 @@ x_7 = l_Lean_mkLet(x_1, x_2, x_3, x_4, x_6);
return x_7;
}
}
lean_object* l_Lean_mkAppB(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = l_Lean_mkApp(x_1, x_2);
x_5 = l_Lean_mkApp(x_4, x_3);
return x_5;
}
}
lean_object* l_Lean_mkApp2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_mkAppB(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_mkApp3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6;
x_5 = l_Lean_mkAppB(x_1, x_2, x_3);
x_6 = l_Lean_mkApp(x_5, x_4);
return x_6;
}
}
lean_object* l_Lean_mkApp4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7;
x_6 = l_Lean_mkAppB(x_1, x_2, x_3);
x_7 = l_Lean_mkAppB(x_6, x_4, x_5);
return x_7;
}
}
lean_object* l_Lean_mkApp5(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;
x_7 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_8 = l_Lean_mkApp(x_7, x_6);
return x_8;
}
}
lean_object* l_Lean_mkApp6(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
x_8 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_9 = l_Lean_mkAppB(x_8, x_6, x_7);
return x_9;
}
}
lean_object* l_Lean_mkApp7(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10;
x_9 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_10 = l_Lean_mkApp3(x_9, x_6, x_7, x_8);
return x_10;
}
}
lean_object* l_Lean_mkApp8(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10; lean_object* x_11;
x_10 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_11 = l_Lean_mkApp4(x_10, x_6, x_7, x_8, x_9);
return x_11;
}
}
lean_object* l_Lean_mkApp9(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_12;
x_11 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_12 = l_Lean_mkApp5(x_11, x_6, x_7, x_8, x_9, x_10);
return x_12;
}
}
lean_object* l_Lean_mkApp10(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
lean_object* x_12; lean_object* x_13;
x_12 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_13 = l_Lean_mkApp6(x_12, x_6, x_7, x_8, x_9, x_10, x_11);
return x_13;
}
}
lean_object* l_Lean_mkLit(lean_object* x_1) {
_start:
{
uint64_t x_2; uint64_t x_3; uint64_t x_4; lean_object* x_5; uint8_t x_6; uint64_t x_7; lean_object* x_8;
x_2 = 3;
x_3 = l_Lean_Literal_hash(x_1);
x_4 = lean_uint64_mix_hash(x_2, x_3);
x_5 = lean_unsigned_to_nat(0u);
x_6 = 0;
x_7 = l_Lean_Expr_mkData(x_4, x_5, x_6, x_6, x_6, x_6);
x_8 = lean_alloc_ctor(9, 1, 8);
lean_ctor_set(x_8, 0, x_1);
lean_ctor_set_uint64(x_8, sizeof(void*)*1, x_7);
return x_8;
}
}
lean_object* l_Lean_mkRawNatLit(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
x_3 = l_Lean_mkLit(x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_mkNatLit___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("OfNat");
return x_1;
}
}
static lean_object* _init_l_Lean_mkNatLit___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_mkNatLit___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_mkNatLit___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("ofNat");
return x_1;
}
}
static lean_object* _init_l_Lean_mkNatLit___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkNatLit___closed__2;
x_2 = l_Lean_mkNatLit___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_mkNatLit___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_levelZero;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_mkNatLit___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_mkNatLit___closed__4;
x_2 = l_Lean_mkNatLit___closed__5;
x_3 = l_Lean_mkConst(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_mkNatLit___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Literal_type___closed__2;
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_mkNatLit___closed__8() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("instOfNatNat");
return x_1;
}
}
static lean_object* _init_l_Lean_mkNatLit___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_mkNatLit___closed__8;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_mkNatLit___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_mkNatLit___closed__9;
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
lean_object* l_Lean_mkNatLit(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_2 = l_Lean_mkRawNatLit(x_1);
x_3 = l_Lean_mkNatLit___closed__10;
lean_inc(x_2);
x_4 = l_Lean_mkApp(x_3, x_2);
x_5 = l_Lean_mkNatLit___closed__6;
x_6 = l_Lean_mkNatLit___closed__7;
x_7 = l_Lean_mkApp3(x_5, x_6, x_2, x_4);
return x_7;
}
}
lean_object* l_Lean_mkStrLit(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
x_3 = l_Lean_mkLit(x_2);
return x_3;
}
}
lean_object* lean_expr_mk_bvar(lean_object* x_1) {
_start:
{
@ -7719,7 +7928,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_getRevArg_x21___closed__1;
x_3 = lean_unsigned_to_nat(485u);
x_3 = lean_unsigned_to_nat(500u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Expr_getRevArg_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -8034,7 +8243,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_appFn_x21___closed__1;
x_3 = lean_unsigned_to_nat(505u);
x_3 = lean_unsigned_to_nat(520u);
x_4 = lean_unsigned_to_nat(17u);
x_5 = l_Lean_Expr_appFn_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -8084,7 +8293,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_appArg_x21___closed__1;
x_3 = lean_unsigned_to_nat(509u);
x_3 = lean_unsigned_to_nat(524u);
x_4 = lean_unsigned_to_nat(17u);
x_5 = l_Lean_Expr_appFn_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -8351,17 +8560,9 @@ return x_3;
static lean_object* _init_l_Lean_Expr_isCharLit___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("ofNat");
return x_1;
}
}
static lean_object* _init_l_Lean_Expr_isCharLit___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Expr_isCharLit___closed__2;
x_2 = l_Lean_Expr_isCharLit___closed__3;
x_2 = l_Lean_mkNatLit___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
@ -8370,7 +8571,7 @@ uint8_t l_Lean_Expr_isCharLit(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = l_Lean_Expr_isCharLit___closed__4;
x_2 = l_Lean_Expr_isCharLit___closed__3;
x_3 = lean_unsigned_to_nat(1u);
x_4 = l_Lean_Expr_isAppOfArity(x_1, x_2, x_3);
if (x_4 == 0)
@ -8421,7 +8622,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_constName_x21___closed__1;
x_3 = lean_unsigned_to_nat(528u);
x_3 = lean_unsigned_to_nat(543u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_constName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -8500,7 +8701,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_constLevels_x21___closed__1;
x_3 = lean_unsigned_to_nat(536u);
x_3 = lean_unsigned_to_nat(551u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_constName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -8558,7 +8759,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_bvarIdx_x21___closed__1;
x_3 = lean_unsigned_to_nat(540u);
x_3 = lean_unsigned_to_nat(555u);
x_4 = lean_unsigned_to_nat(18u);
x_5 = l_Lean_Expr_bvarIdx_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -8616,7 +8817,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_fvarId_x21___closed__1;
x_3 = lean_unsigned_to_nat(544u);
x_3 = lean_unsigned_to_nat(559u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_Expr_fvarId_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -8674,7 +8875,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_mvarId_x21___closed__1;
x_3 = lean_unsigned_to_nat(548u);
x_3 = lean_unsigned_to_nat(563u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_Expr_mvarId_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -8789,7 +8990,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_bindingName_x21___closed__1;
x_3 = lean_unsigned_to_nat(553u);
x_3 = lean_unsigned_to_nat(568u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_bindingName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -8848,7 +9049,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_bindingDomain_x21___closed__1;
x_3 = lean_unsigned_to_nat(558u);
x_3 = lean_unsigned_to_nat(573u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_bindingName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -8907,7 +9108,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_bindingBody_x21___closed__1;
x_3 = lean_unsigned_to_nat(563u);
x_3 = lean_unsigned_to_nat(578u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_bindingName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -8966,7 +9167,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_bindingInfo_x21___closed__1;
x_3 = lean_unsigned_to_nat(568u);
x_3 = lean_unsigned_to_nat(583u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_bindingName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -9037,7 +9238,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_letName_x21___closed__1;
x_3 = lean_unsigned_to_nat(572u);
x_3 = lean_unsigned_to_nat(587u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Expr_letName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -9838,95 +10039,6 @@ x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* l_Lean_mkAppB(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = l_Lean_mkApp(x_1, x_2);
x_5 = l_Lean_mkApp(x_4, x_3);
return x_5;
}
}
lean_object* l_Lean_mkApp2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_mkAppB(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_mkApp3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6;
x_5 = l_Lean_mkAppB(x_1, x_2, x_3);
x_6 = l_Lean_mkApp(x_5, x_4);
return x_6;
}
}
lean_object* l_Lean_mkApp4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7;
x_6 = l_Lean_mkAppB(x_1, x_2, x_3);
x_7 = l_Lean_mkAppB(x_6, x_4, x_5);
return x_7;
}
}
lean_object* l_Lean_mkApp5(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;
x_7 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_8 = l_Lean_mkApp(x_7, x_6);
return x_8;
}
}
lean_object* l_Lean_mkApp6(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
x_8 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_9 = l_Lean_mkAppB(x_8, x_6, x_7);
return x_9;
}
}
lean_object* l_Lean_mkApp7(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10;
x_9 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_10 = l_Lean_mkApp3(x_9, x_6, x_7, x_8);
return x_10;
}
}
lean_object* l_Lean_mkApp8(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10; lean_object* x_11;
x_10 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_11 = l_Lean_mkApp4(x_10, x_6, x_7, x_8, x_9);
return x_11;
}
}
lean_object* l_Lean_mkApp9(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_12;
x_11 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_12 = l_Lean_mkApp5(x_11, x_6, x_7, x_8, x_9, x_10);
return x_12;
}
}
lean_object* l_Lean_mkApp10(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
lean_object* x_12; lean_object* x_13;
x_12 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_13 = l_Lean_mkApp6(x_12, x_6, x_7, x_8, x_9, x_10, x_11);
return x_13;
}
}
static lean_object* _init_l_Lean_mkDecIsTrue___closed__1() {
_start:
{
@ -11532,7 +11644,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateApp_x21___closed__1;
x_3 = lean_unsigned_to_nat(855u);
x_3 = lean_unsigned_to_nat(859u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_appFn_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11604,7 +11716,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateConst_x21___closed__1;
x_3 = lean_unsigned_to_nat(864u);
x_3 = lean_unsigned_to_nat(868u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_constName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11683,7 +11795,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateSort_x21___closed__1;
x_3 = lean_unsigned_to_nat(873u);
x_3 = lean_unsigned_to_nat(877u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_Expr_updateSort_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11767,7 +11879,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateMData_x21___closed__1;
x_3 = lean_unsigned_to_nat(890u);
x_3 = lean_unsigned_to_nat(894u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_updateMData_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11838,7 +11950,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateProj_x21___closed__1;
x_3 = lean_unsigned_to_nat(895u);
x_3 = lean_unsigned_to_nat(899u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Expr_updateProj_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11922,7 +12034,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateForall_x21___closed__1;
x_3 = lean_unsigned_to_nat(904u);
x_3 = lean_unsigned_to_nat(908u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_updateForall_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11999,7 +12111,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateForallE_x21___closed__1;
x_3 = lean_unsigned_to_nat(909u);
x_3 = lean_unsigned_to_nat(913u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Expr_updateForall_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12087,7 +12199,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateLambda_x21___closed__1;
x_3 = lean_unsigned_to_nat(918u);
x_3 = lean_unsigned_to_nat(922u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_updateLambda_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12164,7 +12276,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateLambdaE_x21___closed__1;
x_3 = lean_unsigned_to_nat(923u);
x_3 = lean_unsigned_to_nat(927u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Expr_updateLambda_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -12242,7 +12354,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2;
x_2 = l_Lean_Expr_updateLet_x21___closed__1;
x_3 = lean_unsigned_to_nat(932u);
x_3 = lean_unsigned_to_nat(936u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Expr_letName_x21___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -15656,6 +15768,26 @@ l_Lean_mkSimpleThunk___closed__1 = _init_l_Lean_mkSimpleThunk___closed__1();
lean_mark_persistent(l_Lean_mkSimpleThunk___closed__1);
l_Lean_mkSimpleThunk___closed__2 = _init_l_Lean_mkSimpleThunk___closed__2();
lean_mark_persistent(l_Lean_mkSimpleThunk___closed__2);
l_Lean_mkNatLit___closed__1 = _init_l_Lean_mkNatLit___closed__1();
lean_mark_persistent(l_Lean_mkNatLit___closed__1);
l_Lean_mkNatLit___closed__2 = _init_l_Lean_mkNatLit___closed__2();
lean_mark_persistent(l_Lean_mkNatLit___closed__2);
l_Lean_mkNatLit___closed__3 = _init_l_Lean_mkNatLit___closed__3();
lean_mark_persistent(l_Lean_mkNatLit___closed__3);
l_Lean_mkNatLit___closed__4 = _init_l_Lean_mkNatLit___closed__4();
lean_mark_persistent(l_Lean_mkNatLit___closed__4);
l_Lean_mkNatLit___closed__5 = _init_l_Lean_mkNatLit___closed__5();
lean_mark_persistent(l_Lean_mkNatLit___closed__5);
l_Lean_mkNatLit___closed__6 = _init_l_Lean_mkNatLit___closed__6();
lean_mark_persistent(l_Lean_mkNatLit___closed__6);
l_Lean_mkNatLit___closed__7 = _init_l_Lean_mkNatLit___closed__7();
lean_mark_persistent(l_Lean_mkNatLit___closed__7);
l_Lean_mkNatLit___closed__8 = _init_l_Lean_mkNatLit___closed__8();
lean_mark_persistent(l_Lean_mkNatLit___closed__8);
l_Lean_mkNatLit___closed__9 = _init_l_Lean_mkNatLit___closed__9();
lean_mark_persistent(l_Lean_mkNatLit___closed__9);
l_Lean_mkNatLit___closed__10 = _init_l_Lean_mkNatLit___closed__10();
lean_mark_persistent(l_Lean_mkNatLit___closed__10);
l_Lean_Expr_instBEqExpr___closed__1 = _init_l_Lean_Expr_instBEqExpr___closed__1();
lean_mark_persistent(l_Lean_Expr_instBEqExpr___closed__1);
l_Lean_Expr_instBEqExpr = _init_l_Lean_Expr_instBEqExpr();
@ -15684,8 +15816,6 @@ l_Lean_Expr_isCharLit___closed__2 = _init_l_Lean_Expr_isCharLit___closed__2();
lean_mark_persistent(l_Lean_Expr_isCharLit___closed__2);
l_Lean_Expr_isCharLit___closed__3 = _init_l_Lean_Expr_isCharLit___closed__3();
lean_mark_persistent(l_Lean_Expr_isCharLit___closed__3);
l_Lean_Expr_isCharLit___closed__4 = _init_l_Lean_Expr_isCharLit___closed__4();
lean_mark_persistent(l_Lean_Expr_isCharLit___closed__4);
l_Lean_Expr_constName_x21___closed__1 = _init_l_Lean_Expr_constName_x21___closed__1();
lean_mark_persistent(l_Lean_Expr_constName_x21___closed__1);
l_Lean_Expr_constName_x21___closed__2 = _init_l_Lean_Expr_constName_x21___closed__2();

4
stage0/stdlib/Lean/Meta/AppBuilder.c generated
View file

@ -176,6 +176,7 @@ lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppMFinal(lean_obje
static lean_object* l_Lean_Meta_mkProjection___closed__5;
lean_object* l___private_Lean_Util_Trace_0__Lean_getResetTraces___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_processPostponedStep___spec__6___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkHEqTrans_match__1(lean_object*);
lean_object* l_Lean_mkRawNatLit(lean_object*);
static lean_object* l_Lean_Meta_mkNoConfusion___closed__3;
static lean_object* l_Lean_Meta_mkImpCongrCtx___closed__2;
lean_object* l_Lean_Meta_mkEqSymm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -378,7 +379,6 @@ lean_object* l_Lean_Meta_whnfD(lean_object*, lean_object*, lean_object*, lean_ob
static lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_throwAppBuilderException___rarg___closed__4;
lean_object* l_Lean_Meta_mkFreshLevelMVar___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_mkAppM___closed__3;
lean_object* l_Lean_mkNatLit(lean_object*);
lean_object* l_Lean_Meta_mkHEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_mkEq___closed__1;
static lean_object* l_Lean_Meta_mkEqOfHEq___closed__5;
@ -12891,7 +12891,7 @@ lean_ctor_set(x_12, 1, x_11);
x_13 = l_Lean_Meta_mkNumeral___closed__2;
lean_inc(x_12);
x_14 = l_Lean_mkConst(x_13, x_12);
x_15 = l_Lean_mkNatLit(x_2);
x_15 = l_Lean_mkRawNatLit(x_2);
lean_inc(x_15);
lean_inc(x_1);
x_16 = l_Lean_mkAppB(x_14, x_1, x_15);

12
stage0/stdlib/Lean/Meta/Closure.c generated
View file

@ -4156,7 +4156,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__2;
x_3 = lean_unsigned_to_nat(890u);
x_3 = lean_unsigned_to_nat(894u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -4185,7 +4185,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__5;
x_3 = lean_unsigned_to_nat(895u);
x_3 = lean_unsigned_to_nat(899u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__6;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -4214,7 +4214,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__8;
x_3 = lean_unsigned_to_nat(855u);
x_3 = lean_unsigned_to_nat(859u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__9;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -4243,7 +4243,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__11;
x_3 = lean_unsigned_to_nat(923u);
x_3 = lean_unsigned_to_nat(927u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__12;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -4272,7 +4272,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__14;
x_3 = lean_unsigned_to_nat(909u);
x_3 = lean_unsigned_to_nat(913u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__15;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -4301,7 +4301,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_Closure_collectExprAux___closed__1;
x_2 = l_Lean_Meta_Closure_collectExprAux___closed__17;
x_3 = lean_unsigned_to_nat(932u);
x_3 = lean_unsigned_to_nat(936u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Meta_Closure_collectExprAux___closed__18;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@ -14721,7 +14721,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_CheckAssignment_check___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_check___closed__2;
x_3 = lean_unsigned_to_nat(890u);
x_3 = lean_unsigned_to_nat(894u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Meta_CheckAssignment_check___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -14750,7 +14750,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_CheckAssignment_check___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_check___closed__5;
x_3 = lean_unsigned_to_nat(895u);
x_3 = lean_unsigned_to_nat(899u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Meta_CheckAssignment_check___closed__6;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -14779,7 +14779,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_CheckAssignment_check___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_check___closed__8;
x_3 = lean_unsigned_to_nat(923u);
x_3 = lean_unsigned_to_nat(927u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Meta_CheckAssignment_check___closed__9;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -14808,7 +14808,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_CheckAssignment_check___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_check___closed__11;
x_3 = lean_unsigned_to_nat(909u);
x_3 = lean_unsigned_to_nat(913u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Meta_CheckAssignment_check___closed__12;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -14837,7 +14837,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_CheckAssignment_check___closed__1;
x_2 = l_Lean_Meta_CheckAssignment_check___closed__14;
x_3 = lean_unsigned_to_nat(932u);
x_3 = lean_unsigned_to_nat(936u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Meta_CheckAssignment_check___closed__15;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

10
stage0/stdlib/Lean/Meta/Match/CaseArraySizes.c generated
View file

@ -56,6 +56,7 @@ lean_object* l_Lean_Meta_getMVarType(lean_object*, lean_object*, lean_object*, l
static lean_object* l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_introArrayLit_loop___closed__3;
lean_object* l_Lean_Meta_caseArraySizes_match__1___rarg(lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_mkRawNatLit(lean_object*);
lean_object* l_Lean_Meta_getArrayArgType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkEqSymm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_getArrayArgType___closed__5;
@ -108,7 +109,6 @@ lean_object* l_Lean_Meta_caseArraySizes_match__1(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_caseArraySizes___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_introArrayLit_loop___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_whnfD(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkNatLit(lean_object*);
lean_object* l_Lean_Meta_mkFreshExprSyntheticOpaqueMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapIdxM_map___at_Lean_Meta_caseArraySizes___spec__3___boxed(lean_object**);
@ -427,8 +427,8 @@ lean_object* l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_mkArrayGetL
_start:
{
lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_10 = l_Lean_mkNatLit(x_2);
x_11 = l_Lean_mkNatLit(x_3);
x_10 = l_Lean_mkRawNatLit(x_2);
x_11 = l_Lean_mkRawNatLit(x_3);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
@ -797,7 +797,7 @@ lean_inc(x_21);
x_22 = lean_ctor_get(x_20, 1);
lean_inc(x_22);
lean_dec(x_20);
x_23 = l_Lean_mkNatLit(x_3);
x_23 = l_Lean_mkRawNatLit(x_3);
x_24 = l___private_Lean_Meta_Match_CaseArraySizes_0__Lean_Meta_introArrayLit_loop___closed__3;
x_25 = lean_array_push(x_24, x_2);
x_26 = lean_array_push(x_25, x_23);
@ -1221,7 +1221,7 @@ x_6 = lean_array_uget(x_3, x_2);
x_7 = lean_unsigned_to_nat(0u);
x_8 = lean_array_uset(x_3, x_2, x_7);
x_9 = x_6;
x_10 = l_Lean_mkNatLit(x_9);
x_10 = l_Lean_mkRawNatLit(x_9);
x_11 = 1;
x_12 = x_2 + x_11;
x_13 = x_10;

12
stage0/stdlib/Lean/Meta/Match/Match.c generated
View file

@ -353,6 +353,7 @@ lean_object* l_List_forIn_loop___at___private_Lean_Meta_Match_Match_0__Lean_Meta
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processAsPattern___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_hasArrayLitPattern(lean_object*);
static lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_withAlts_loop___rarg___lambda__1___closed__1;
lean_object* l_Lean_mkRawNatLit(lean_object*);
lean_object* l_Lean_Meta_Match_mkMatcher___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Match_processInaccessibleAsCtor___closed__2;
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_throwCasesException_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -815,7 +816,6 @@ lean_object* l_Lean_Meta_Match_mkMatcherAuxDefinition___lambda__5(lean_object*,
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processValue(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Match_mkMatcher___lambda__5___closed__3;
static lean_object* l_Lean_Meta_Match_mkMatcher___lambda__5___closed__7;
lean_object* l_Lean_mkNatLit(lean_object*);
lean_object* l_Std_HashSetImp_expand___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_processLeaf___spec__4(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process_tryToProcess(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn(lean_object*);
@ -18524,7 +18524,7 @@ x_28 = lean_unsigned_to_nat(1u);
x_29 = lean_nat_sub(x_25, x_28);
lean_dec(x_25);
x_30 = lean_box(0);
x_31 = l_Lean_mkNatLit(x_29);
x_31 = l_Lean_mkRawNatLit(x_29);
lean_ctor_set(x_12, 0, x_31);
lean_ctor_set(x_10, 1, x_30);
x_32 = l_List_map___at___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_expandNatValuePattern___spec__1___closed__4;
@ -18570,7 +18570,7 @@ x_40 = lean_unsigned_to_nat(1u);
x_41 = lean_nat_sub(x_37, x_40);
lean_dec(x_37);
x_42 = lean_box(0);
x_43 = l_Lean_mkNatLit(x_41);
x_43 = l_Lean_mkRawNatLit(x_41);
lean_ctor_set(x_12, 0, x_43);
x_44 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_44, 0, x_12);
@ -18630,7 +18630,7 @@ x_55 = lean_unsigned_to_nat(1u);
x_56 = lean_nat_sub(x_52, x_55);
lean_dec(x_52);
x_57 = lean_box(0);
x_58 = l_Lean_mkNatLit(x_56);
x_58 = l_Lean_mkRawNatLit(x_56);
lean_ctor_set(x_12, 0, x_58);
if (lean_is_scalar(x_51)) {
x_59 = lean_alloc_ctor(1, 2, 0);
@ -18797,7 +18797,7 @@ x_83 = lean_unsigned_to_nat(1u);
x_84 = lean_nat_sub(x_80, x_83);
lean_dec(x_80);
x_85 = lean_box(0);
x_86 = l_Lean_mkNatLit(x_84);
x_86 = l_Lean_mkRawNatLit(x_84);
x_87 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_87, 0, x_86);
if (lean_is_scalar(x_79)) {
@ -19035,7 +19035,7 @@ x_123 = lean_unsigned_to_nat(1u);
x_124 = lean_nat_sub(x_120, x_123);
lean_dec(x_120);
x_125 = lean_box(0);
x_126 = l_Lean_mkNatLit(x_124);
x_126 = l_Lean_mkRawNatLit(x_124);
if (lean_is_scalar(x_115)) {
x_127 = lean_alloc_ctor(3, 1, 0);
} else {

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

@ -10428,7 +10428,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_SimpLemma_getValue___closed__1;
x_2 = l_Lean_Meta_SimpLemma_getValue___closed__2;
x_3 = lean_unsigned_to_nat(864u);
x_3 = lean_unsigned_to_nat(868u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Meta_SimpLemma_getValue___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

10
stage0/stdlib/Lean/Meta/Transform.c generated
View file

@ -873,7 +873,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__2;
x_3 = lean_unsigned_to_nat(923u);
x_3 = lean_unsigned_to_nat(927u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -980,7 +980,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__4___closed__1;
x_3 = lean_unsigned_to_nat(909u);
x_3 = lean_unsigned_to_nat(913u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__4___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -1087,7 +1087,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__6___closed__1;
x_3 = lean_unsigned_to_nat(932u);
x_3 = lean_unsigned_to_nat(936u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__6___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -1225,7 +1225,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__9___closed__1;
x_3 = lean_unsigned_to_nat(890u);
x_3 = lean_unsigned_to_nat(894u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__9___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -1299,7 +1299,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Core_transform_visit___rarg___lambda__2___closed__1;
x_2 = l_Lean_Core_transform_visit___rarg___lambda__10___closed__1;
x_3 = lean_unsigned_to_nat(895u);
x_3 = lean_unsigned_to_nat(899u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_Core_transform_visit___rarg___lambda__10___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@ -176,6 +176,7 @@ lean_object* l___private_Lean_Meta_WHNF_0__Lean_Meta_useWHNFCache(lean_object*,
lean_object* l_Lean_Meta_reduceRecMatcher_x3f___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_WHNF_0__Lean_Meta_reduceRec___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_toCtorIfLit___closed__3;
lean_object* l_Lean_mkRawNatLit(lean_object*);
lean_object* l_Lean_Expr_headBeta(lean_object*);
lean_object* l___private_Lean_Meta_WHNF_0__Lean_Meta_isRecStuck_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_whnfHeadPred___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1732,7 +1733,7 @@ lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_obj
x_6 = lean_unsigned_to_nat(1u);
x_7 = lean_nat_sub(x_3, x_6);
lean_dec(x_3);
x_8 = l_Lean_mkNatLit(x_7);
x_8 = l_Lean_mkRawNatLit(x_7);
x_9 = l_Lean_Meta_toCtorIfLit___closed__5;
x_10 = l_Lean_mkApp(x_9, x_8);
return x_10;
@ -16427,7 +16428,7 @@ else
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_23 = lean_unsigned_to_nat(0u);
x_24 = lean_apply_1(x_1, x_23);
x_25 = l_Lean_mkNatLit(x_24);
x_25 = l_Lean_mkRawNatLit(x_24);
x_26 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_8, 0, x_26);
@ -16482,7 +16483,7 @@ else
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42;
x_38 = lean_unsigned_to_nat(0u);
x_39 = lean_apply_1(x_1, x_38);
x_40 = l_Lean_mkNatLit(x_39);
x_40 = l_Lean_mkRawNatLit(x_39);
x_41 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_41, 0, x_40);
x_42 = lean_alloc_ctor(0, 2, 0);
@ -16602,7 +16603,7 @@ x_64 = lean_ctor_get(x_61, 0);
lean_inc(x_64);
lean_dec(x_61);
x_65 = lean_apply_1(x_1, x_64);
x_66 = l_Lean_mkNatLit(x_65);
x_66 = l_Lean_mkRawNatLit(x_65);
x_67 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_67, 0, x_66);
lean_ctor_set(x_8, 0, x_67);
@ -16618,7 +16619,7 @@ x_69 = lean_ctor_get(x_61, 0);
lean_inc(x_69);
lean_dec(x_61);
x_70 = lean_apply_1(x_1, x_69);
x_71 = l_Lean_mkNatLit(x_70);
x_71 = l_Lean_mkRawNatLit(x_70);
x_72 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_72, 0, x_71);
x_73 = lean_alloc_ctor(0, 2, 0);
@ -16717,7 +16718,7 @@ _start:
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_8 = lean_unsigned_to_nat(0u);
x_9 = lean_apply_2(x_1, x_8, x_8);
x_10 = l_Lean_mkNatLit(x_9);
x_10 = l_Lean_mkRawNatLit(x_9);
x_11 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_11, 0, x_10);
x_12 = lean_alloc_ctor(0, 2, 0);
@ -16732,7 +16733,7 @@ _start:
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_9 = lean_unsigned_to_nat(0u);
x_10 = lean_apply_2(x_1, x_9, x_2);
x_11 = l_Lean_mkNatLit(x_10);
x_11 = l_Lean_mkRawNatLit(x_10);
x_12 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_12, 0, x_11);
x_13 = lean_alloc_ctor(0, 2, 0);
@ -16747,7 +16748,7 @@ _start:
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_9 = lean_unsigned_to_nat(0u);
x_10 = lean_apply_2(x_1, x_2, x_9);
x_11 = l_Lean_mkNatLit(x_10);
x_11 = l_Lean_mkRawNatLit(x_10);
x_12 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_12, 0, x_11);
x_13 = lean_alloc_ctor(0, 2, 0);
@ -16761,7 +16762,7 @@ _start:
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_10 = lean_apply_2(x_1, x_2, x_3);
x_11 = l_Lean_mkNatLit(x_10);
x_11 = l_Lean_mkRawNatLit(x_10);
x_12 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_12, 0, x_11);
x_13 = lean_alloc_ctor(0, 2, 0);

14
stage0/stdlib/Lean/MetavarContext.c generated
View file

@ -11117,7 +11117,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__2;
x_3 = lean_unsigned_to_nat(873u);
x_3 = lean_unsigned_to_nat(877u);
x_4 = lean_unsigned_to_nat(16u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11200,7 +11200,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__11___closed__1;
x_3 = lean_unsigned_to_nat(864u);
x_3 = lean_unsigned_to_nat(868u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__11___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11286,7 +11286,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__12___closed__1;
x_3 = lean_unsigned_to_nat(923u);
x_3 = lean_unsigned_to_nat(927u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__12___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11393,7 +11393,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__14___closed__1;
x_3 = lean_unsigned_to_nat(909u);
x_3 = lean_unsigned_to_nat(913u);
x_4 = lean_unsigned_to_nat(23u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__14___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11500,7 +11500,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__16___closed__1;
x_3 = lean_unsigned_to_nat(932u);
x_3 = lean_unsigned_to_nat(936u);
x_4 = lean_unsigned_to_nat(22u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__16___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11634,7 +11634,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__19___closed__1;
x_3 = lean_unsigned_to_nat(890u);
x_3 = lean_unsigned_to_nat(894u);
x_4 = lean_unsigned_to_nat(19u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__19___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -11720,7 +11720,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__10___closed__1;
x_2 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__20___closed__1;
x_3 = lean_unsigned_to_nat(895u);
x_3 = lean_unsigned_to_nat(899u);
x_4 = lean_unsigned_to_nat(20u);
x_5 = l_Lean_MetavarContext_instantiateExprMVars___rarg___lambda__20___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@ -261,6 +261,7 @@ lean_object* l_Lean_Parser_nonReservedSymbolInfo(lean_object*, uint8_t);
lean_object* l_Lean_Parser_ParserExtension_instInhabitedState;
static lean_object* l___private_Lean_Parser_Extension_0__Lean_Parser_registerParserAttributeImplBuilder___closed__1;
static lean_object* l_Lean_Parser_parserExtension___closed__6;
lean_object* l_Lean_mkRawNatLit(lean_object*);
lean_object* l_List_forM___at___private_Lean_Parser_Extension_0__Lean_Parser_ParserAttribute_add___spec__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkParserOfConstantUnsafe(lean_object*);
lean_object* l_Lean_registerAttributeOfBuilder(lean_object*, lean_object*, lean_object*, lean_object*);
@ -541,7 +542,6 @@ static lean_object* l_Std_PersistentHashMap_foldlMAux___at_Lean_Parser_getSyntax
lean_object* l_Lean_Parser_addLeadingParser_match__2(lean_object*);
lean_object* l_Std_PersistentHashMap_foldlM___at___private_Lean_Parser_Extension_0__Lean_Parser_ParserAttribute_add___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_getParserPriority___closed__3;
lean_object* l_Lean_mkNatLit(lean_object*);
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_2883____closed__5;
static lean_object* l_Lean_Parser_initFn____x40_Lean_Parser_Extension___hyg_4322____closed__4;
lean_object* l_Std_PersistentHashMap_find_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -10422,7 +10422,7 @@ lean_inc(x_4);
x_12 = l_Lean_Name_toExprAux(x_4);
lean_inc(x_4);
x_13 = l_Lean_mkConst(x_4, x_9);
x_14 = l_Lean_mkNatLit(x_5);
x_14 = l_Lean_mkRawNatLit(x_5);
x_15 = l_Lean_Parser_declareBuiltinParser___closed__10;
x_16 = lean_array_push(x_15, x_11);
x_17 = lean_array_push(x_16, x_12);

1738
stage0/stdlib/Lean/Structure.c generated
View file

File diff suppressed because it is too large Load diff

108
stage0/stdlib/Std/Data/PersistentHashMap.c generated
View file

@ -61,7 +61,6 @@ lean_object* l_Std_PersistentHashMap_getCollisionNodeSize___rarg(lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Std_PersistentHashMap_toList___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_getCollisionNodeSize_match__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_collectStats_match__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_max(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_insert(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_getCollisionNodeSize(lean_object*, lean_object*);
@ -90,6 +89,7 @@ lean_object* l_Std_PersistentHashMap_empty___rarg(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_erase_match__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_PersistentHashMap_find_x21___rarg___closed__4;
lean_object* l_Std_PersistentHashMap_foldlMAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_containsAux_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_foldl___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Std_PersistentHashMap_toList___spec__3___rarg(lean_object*, size_t, size_t, lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
@ -134,7 +134,7 @@ lean_object* l_Std_PersistentHashMap_containsAtAux___rarg___boxed(lean_object*,
lean_object* l_Std_PersistentHashMap_collectStats(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_getCollisionNodeSize_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_findEntry_x3f(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_collectStats_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_collectStats_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_foldlMAux___at_Std_PersistentHashMap_toList___spec__2___rarg(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_stats___rarg(lean_object*);
lean_object* l_Std_PersistentHashMap_forM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -200,7 +200,7 @@ lean_object* l_Std_PersistentHashMap_eraseAux___rarg___boxed(lean_object*, lean_
lean_object* l_Std_PersistentHashMap_isUnaryNode_match__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_isEmpty___rarg___boxed(lean_object*);
lean_object* l_Std_PersistentHashMap_contains(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_collectStats_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_containsAux_match__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_PersistentHashMap_Stats_toString___closed__5;
lean_object* l_Std_PersistentHashMap_insert_match__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_findD(lean_object*, lean_object*);
@ -2213,6 +2213,54 @@ x_8 = lean_box(x_7);
return x_8;
}
}
lean_object* l_Std_PersistentHashMap_containsAux_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
switch (lean_obj_tag(x_1)) {
case 0:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
lean_dec(x_3);
lean_dec(x_2);
x_5 = lean_ctor_get(x_1, 0);
lean_inc(x_5);
x_6 = lean_ctor_get(x_1, 1);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_apply_2(x_4, x_5, x_6);
return x_7;
}
case 1:
{
lean_object* x_8; lean_object* x_9;
lean_dec(x_4);
lean_dec(x_2);
x_8 = lean_ctor_get(x_1, 0);
lean_inc(x_8);
lean_dec(x_1);
x_9 = lean_apply_1(x_3, x_8);
return x_9;
}
default:
{
lean_object* x_10; lean_object* x_11;
lean_dec(x_4);
lean_dec(x_3);
x_10 = lean_box(0);
x_11 = lean_apply_1(x_2, x_10);
return x_11;
}
}
}
}
lean_object* l_Std_PersistentHashMap_containsAux_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Std_PersistentHashMap_containsAux_match__1___rarg), 4, 0);
return x_4;
}
}
lean_object* l_Std_PersistentHashMap_containsAux___rarg(lean_object* x_1, lean_object* x_2, size_t x_3, lean_object* x_4) {
_start:
{
@ -4129,55 +4177,7 @@ x_1 = lean_unsigned_to_nat(0u);
return x_1;
}
}
lean_object* l_Std_PersistentHashMap_collectStats_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
switch (lean_obj_tag(x_1)) {
case 0:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
lean_dec(x_3);
lean_dec(x_2);
x_5 = lean_ctor_get(x_1, 0);
lean_inc(x_5);
x_6 = lean_ctor_get(x_1, 1);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_apply_2(x_4, x_5, x_6);
return x_7;
}
case 1:
{
lean_object* x_8; lean_object* x_9;
lean_dec(x_4);
lean_dec(x_2);
x_8 = lean_ctor_get(x_1, 0);
lean_inc(x_8);
lean_dec(x_1);
x_9 = lean_apply_1(x_3, x_8);
return x_9;
}
default:
{
lean_object* x_10; lean_object* x_11;
lean_dec(x_4);
lean_dec(x_3);
x_10 = lean_box(0);
x_11 = lean_apply_1(x_2, x_10);
return x_11;
}
}
}
}
lean_object* l_Std_PersistentHashMap_collectStats_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Std_PersistentHashMap_collectStats_match__1___rarg), 4, 0);
return x_4;
}
}
lean_object* l_Std_PersistentHashMap_collectStats_match__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
lean_object* l_Std_PersistentHashMap_collectStats_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
if (lean_obj_tag(x_1) == 0)
@ -4204,11 +4204,11 @@ return x_10;
}
}
}
lean_object* l_Std_PersistentHashMap_collectStats_match__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Std_PersistentHashMap_collectStats_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Std_PersistentHashMap_collectStats_match__2___rarg), 5, 0);
x_4 = lean_alloc_closure((void*)(l_Std_PersistentHashMap_collectStats_match__1___rarg), 5, 0);
return x_4;
}
}