diff --git a/stage0/src/Init/Data/Array/Basic.lean b/stage0/src/Init/Data/Array/Basic.lean index 9850d33195..9387803c81 100644 --- a/stage0/src/Init/Data/Array/Basic.lean +++ b/stage0/src/Init/Data/Array/Basic.lean @@ -166,8 +166,8 @@ def shrink {α : Type u} (a : Array α) (n : Nat) : Array α := loop (a.size - n) a @[inline] -def modifyM {m : Type u → Type v} [Monad m] [Inhabited α] (a : Array α) (i : Nat) (f : α → m α) : m (Array α) := - if h : i < a.size then do +def modifyM {m : Type u → Type v} [Monad m] [Inhabited α] (a : Array α) (i : Nat) (f : α → m α) : m (Array α) := do + if h : i < a.size then let idx : Fin a.size := ⟨i, h⟩ let v := a.get idx let a := a.set idx (arbitrary α) @@ -389,8 +389,8 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : any as.size (Nat.leRefl _) @[inline] -def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m Bool := do - return !(← as.anyM fun v => do return !(← p v)) +def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m Bool := + return !(← as.anyM fun v => return !(← p v)) @[inline] def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β) := @@ -408,7 +408,7 @@ def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] @[inline] def findRevM? {α : Type} {m : Type → Type w} [Monad m] (as : Array α) (p : α → m Bool) : m (Option α) := - as.findSomeRevM? fun a => do return if (← p a) then some a else none + as.findSomeRevM? fun a => return if (← p a) then some a else none @[inline] def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start := 0) (stop := as.size) : m PUnit := diff --git a/stage0/src/Init/Data/List/Control.lean b/stage0/src/Init/Data/List/Control.lean index 3040a30578..8da46ebcae 100644 --- a/stage0/src/Init/Data/List/Control.lean +++ b/stage0/src/Init/Data/List/Control.lean @@ -44,7 +44,7 @@ Users that want to use `mapM` with `Applicative` should use `mapA` instead. @[specialize] def mapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β) | [] => pure [] - | a::as => do return (← f a) :: (← mapM f as) + | a::as => return (← f a) :: (← mapM f as) @[specialize] def mapA {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β) diff --git a/stage0/src/Lean/Compiler/IR/ElimDeadBranches.lean b/stage0/src/Lean/Compiler/IR/ElimDeadBranches.lean index 09330522af..b097ecd3dd 100644 --- a/stage0/src/Lean/Compiler/IR/ElimDeadBranches.lean +++ b/stage0/src/Lean/Compiler/IR/ElimDeadBranches.lean @@ -150,8 +150,8 @@ partial def projValue : Value → Nat → Value | v, _ => v def interpExpr : Expr → M Value - | Expr.ctor i ys => do return ctor i (← ys.mapM fun y => findArgValue y) - | Expr.proj i x => do return projValue (← findVarValue x) i + | Expr.ctor i ys => return ctor i (← ys.mapM fun y => findArgValue y) + | Expr.proj i x => return projValue (← findVarValue x) i | Expr.fap fid ys => do let ctx ← read match getFunctionSummary? ctx.env fid with diff --git a/stage0/src/Lean/Compiler/IR/NormIds.lean b/stage0/src/Lean/Compiler/IR/NormIds.lean index 26d0b15c82..d4f20b2a41 100644 --- a/stage0/src/Lean/Compiler/IR/NormIds.lean +++ b/stage0/src/Lean/Compiler/IR/NormIds.lean @@ -92,24 +92,24 @@ instance : MonadLift M N := ⟨fun x m => pure $ x m⟩ partial def normFnBody : FnBody → N FnBody - | FnBody.vdecl x t v b => do let v ← normExpr v; withVar x fun x => do return FnBody.vdecl x t v (← normFnBody b) + | FnBody.vdecl x t v b => do let v ← normExpr v; withVar x fun x => return FnBody.vdecl x t v (← normFnBody b) | FnBody.jdecl j ys v b => do let (ys, v) ← withParams ys fun ys => do let v ← normFnBody v; pure (ys, v) - withJP j fun j => do return FnBody.jdecl j ys v (← normFnBody b) - | FnBody.set x i y b => do return FnBody.set (← normVar x) i (← normArg y) (← normFnBody b) - | FnBody.uset x i y b => do return FnBody.uset (← normVar x) i (← normVar y) (← normFnBody b) - | FnBody.sset x i o y t b => do return FnBody.sset (← normVar x) i o (← normVar y) t (← normFnBody b) - | FnBody.setTag x i b => do return FnBody.setTag (← normVar x) i (← normFnBody b) - | FnBody.inc x n c p b => do return FnBody.inc (← normVar x) n c p (← normFnBody b) - | FnBody.dec x n c p b => do return FnBody.dec (← normVar x) n c p (← normFnBody b) - | FnBody.del x b => do return FnBody.del (← normVar x) (← normFnBody b) - | FnBody.mdata d b => do return FnBody.mdata d (← normFnBody b) + withJP j fun j => return FnBody.jdecl j ys v (← normFnBody b) + | FnBody.set x i y b => return FnBody.set (← normVar x) i (← normArg y) (← normFnBody b) + | FnBody.uset x i y b => return FnBody.uset (← normVar x) i (← normVar y) (← normFnBody b) + | FnBody.sset x i o y t b => return FnBody.sset (← normVar x) i o (← normVar y) t (← normFnBody b) + | FnBody.setTag x i b => return FnBody.setTag (← normVar x) i (← normFnBody b) + | FnBody.inc x n c p b => return FnBody.inc (← normVar x) n c p (← normFnBody b) + | FnBody.dec x n c p b => return FnBody.dec (← normVar x) n c p (← normFnBody b) + | FnBody.del x b => return FnBody.del (← normVar x) (← normFnBody b) + | FnBody.mdata d b => return FnBody.mdata d (← normFnBody b) | FnBody.case tid x xType alts => do let x ← normVar x let alts ← alts.mapM fun alt => alt.mmodifyBody normFnBody return FnBody.case tid x xType alts - | FnBody.jmp j ys => do return FnBody.jmp (← normJP j) (← normArgs ys) - | FnBody.ret x => do return FnBody.ret (← normArg x) + | FnBody.jmp j ys => return FnBody.jmp (← normJP j) (← normArgs ys) + | FnBody.ret x => return FnBody.ret (← normArg x) | FnBody.unreachable => pure FnBody.unreachable def normDecl : Decl → N Decl diff --git a/stage0/src/Lean/Elab/App.lean b/stage0/src/Lean/Elab/App.lean index 46e2daf4c5..038c2178b8 100644 --- a/stage0/src/Lean/Elab/App.lean +++ b/stage0/src/Lean/Elab/App.lean @@ -74,7 +74,7 @@ private def tryCoeFun? (α : Expr) (a : Expr) : TermElabM (Option Expr) := do catch _ => pure none -def synthesizeAppInstMVars (instMVars : Array MVarId) : TermElabM Unit := do +def synthesizeAppInstMVars (instMVars : Array MVarId) : TermElabM Unit := for mvarId in instMVars do unless (← synthesizeInstMVarCore mvarId) do registerSyntheticMVarWithCurrRef mvarId SyntheticMVarKind.typeClass @@ -141,10 +141,10 @@ private def normalizeFunType : M Expr := do pure fType /- Return the binder name at `fType`. This method assumes `fType` is a function type. -/ -private def getBindingName : M Name := do return (← get).fType.bindingName! +private def getBindingName : M Name := return (← get).fType.bindingName! /- Return the next argument expected type. This method assumes `fType` is a function type. -/ -private def getArgExpectedType : M Expr := do return (← get).fType.bindingDomain! +private def getArgExpectedType : M Expr := return (← get).fType.bindingDomain! def eraseNamedArgCore (namedArgs : List NamedArg) (binderName : Name) : List NamedArg := namedArgs.filter (·.name != binderName) diff --git a/stage0/src/Lean/Elab/BuiltinNotation.lean b/stage0/src/Lean/Elab/BuiltinNotation.lean index ace42a2d48..586691db15 100644 --- a/stage0/src/Lean/Elab/BuiltinNotation.lean +++ b/stage0/src/Lean/Elab/BuiltinNotation.lean @@ -51,7 +51,7 @@ open Meta @[builtinTermElab borrowed] def elabBorrowed : TermElab := fun stx expectedType? => match_syntax stx with - | `(@& $e) => do return markBorrowed (← elabTerm e expectedType?) + | `(@& $e) => return markBorrowed (← elabTerm e expectedType?) | _ => throwUnsupportedSyntax @[builtinMacro Lean.Parser.Term.show] def expandShow : Macro := fun stx => diff --git a/stage0/src/Lean/Elab/Command.lean b/stage0/src/Lean/Elab/Command.lean index 4e8b9a9c68..06ebedd2b0 100644 --- a/stage0/src/Lean/Elab/Command.lean +++ b/stage0/src/Lean/Elab/Command.lean @@ -107,7 +107,7 @@ def liftCoreM {α} (x : CoreM α) : CommandElabM α := do let s ← get let ctx ← read let Eα := Except Exception α - let x : CoreM Eα := do try let a ← x; pure $ Except.ok a catch ex => pure $ Except.error ex + let x : CoreM Eα := try let a ← x; pure $ Except.ok a catch ex => pure $ Except.error ex let x : EIO Exception (Eα × Core.State) := (ReaderT.run x (mkCoreContext ctx s)).run { env := s.env, ngen := s.ngen } let (ea, coreS) ← liftM x modify fun s => { s with env := coreS.env, ngen := coreS.ngen } diff --git a/stage0/src/Lean/Elab/Do.lean b/stage0/src/Lean/Elab/Do.lean index ef00fee683..783e5e27d1 100644 --- a/stage0/src/Lean/Elab/Do.lean +++ b/stage0/src/Lean/Elab/Do.lean @@ -1155,9 +1155,10 @@ private partial def expandLiftMethodAux : Syntax → StateT (List Syntax) MacroM pure $ Syntax.node k args | stx => pure stx -def expandLiftMethod (doElem : Syntax) : MacroM (List Syntax × Syntax) := - if !hasLiftMethod doElem then pure ([], doElem) - else do +def expandLiftMethod (doElem : Syntax) : MacroM (List Syntax × Syntax) := do + if !hasLiftMethod doElem then + pure ([], doElem) + else let (doElem, doElemsNew) ← (expandLiftMethodAux doElem).run [] pure (doElemsNew, doElem) diff --git a/stage0/src/Lean/Elab/Level.lean b/stage0/src/Lean/Elab/Level.lean index 568e492593..4e0a0d43c1 100644 --- a/stage0/src/Lean/Elab/Level.lean +++ b/stage0/src/Lean/Elab/Level.lean @@ -20,7 +20,7 @@ structure State := abbrev LevelElabM := ReaderT Context (EStateM Exception State) instance : Ref LevelElabM := { - getRef := do return (← read).ref, + getRef := return (← read).ref, withRef := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x } @@ -29,7 +29,7 @@ instance : AddMessageContext LevelElabM := { } instance : MonadNameGenerator LevelElabM := { - getNGen := do return (← get).ngen, + getNGen := return (← get).ngen, setNGen := fun ngen => modify fun s => { s with ngen := ngen } } diff --git a/stage0/src/Lean/Elab/StructInst.lean b/stage0/src/Lean/Elab/StructInst.lean index 363738c70c..9ece666428 100644 --- a/stage0/src/Lean/Elab/StructInst.lean +++ b/stage0/src/Lean/Elab/StructInst.lean @@ -712,20 +712,21 @@ partial def tryToSynthesizeDefault (structs : Array Struct) (allStructNames : Ar pure false loop 0 0 -partial def step (struct : Struct) : M Unit := do - unlessM isRoundDone $ withReader (fun ctx => { ctx with structs := ctx.structs.push struct }) do - struct.fields.forM fun field => do - match field.val with - | FieldVal.nested struct => step struct - | _ => match field.expr? with - | none => unreachable! - | some expr => match defaultMissing? expr with - | some (Expr.mvar mvarId _) => - unless (← isExprMVarAssigned mvarId) do - let ctx ← read - if (← withRef field.ref $ tryToSynthesizeDefault ctx.structs ctx.allStructNames ctx.maxDistance (getFieldName field) mvarId) then - modify fun s => { s with progress := true } - | _ => pure () +partial def step (struct : Struct) : M Unit := + unless (← isRoundDone) do + withReader (fun ctx => { ctx with structs := ctx.structs.push struct }) do + for field in struct.fields do + match field.val with + | FieldVal.nested struct => step struct + | _ => match field.expr? with + | none => unreachable! + | some expr => match defaultMissing? expr with + | some (Expr.mvar mvarId _) => + unless (← isExprMVarAssigned mvarId) do + let ctx ← read + if (← withRef field.ref $ tryToSynthesizeDefault ctx.structs ctx.allStructNames ctx.maxDistance (getFieldName field) mvarId) then + modify fun s => { s with progress := true } + | _ => pure () partial def propagateLoop (hierarchyDepth : Nat) (d : Nat) (struct : Struct) : M Unit := do match findDefaultMissing? (← getMCtx) struct with diff --git a/stage0/src/Lean/Elab/Tactic/Basic.lean b/stage0/src/Lean/Elab/Tactic/Basic.lean index 82b381783e..b7d2141d41 100644 --- a/stage0/src/Lean/Elab/Tactic/Basic.lean +++ b/stage0/src/Lean/Elab/Tactic/Basic.lean @@ -286,7 +286,7 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit := @[builtinTactic failIfSuccess] def evalFailIfSuccess : Tactic := fun stx => do let tactic := stx[1] - if (← do try evalTactic tactic; pure true catch _ => pure false) then + if (← try evalTactic tactic; pure true catch _ => pure false) then throwError "tactic succeeded" @[builtinTactic traceState] def evalTraceState : Tactic := fun stx => do diff --git a/stage0/src/Lean/Elab/Tactic/ElabTerm.lean b/stage0/src/Lean/Elab/Tactic/ElabTerm.lean index acf59b7b3a..868775ff7d 100644 --- a/stage0/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/stage0/src/Lean/Elab/Tactic/ElabTerm.lean @@ -40,13 +40,13 @@ def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : let val ← elabTermEnsuringType stx expectedType? let newMVarIds ← getMVarsNoDelayed val /- ignore let-rec auxiliary variables, they are synthesized automatically later -/ - let newMVarIds ← newMVarIds.filterM fun mvarId => do return !(← Term.isLetRecAuxMVar mvarId) + let newMVarIds ← newMVarIds.filterM fun mvarId => return !(← Term.isLetRecAuxMVar mvarId) let newMVarIds ← if allowNaturalHoles then pure newMVarIds.toList else - let naturalMVarIds ← newMVarIds.filterM fun mvarId => do return (← getMVarDecl mvarId).kind.isNatural - let syntheticMVarIds ← newMVarIds.filterM fun mvarId => do return !(← getMVarDecl mvarId).kind.isNatural + let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← getMVarDecl mvarId).kind.isNatural + let syntheticMVarIds ← newMVarIds.filterM fun mvarId => return !(← getMVarDecl mvarId).kind.isNatural Term.logUnassignedUsingErrorInfos naturalMVarIds pure syntheticMVarIds.toList tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds diff --git a/stage0/src/Lean/Elab/Tactic/Induction.lean b/stage0/src/Lean/Elab/Tactic/Induction.lean index f9698936d0..8abf55ad5c 100644 --- a/stage0/src/Lean/Elab/Tactic/Induction.lean +++ b/stage0/src/Lean/Elab/Tactic/Induction.lean @@ -92,7 +92,7 @@ private def getAltRHS (alt : Syntax) : Syntax := alt[3] ``` esnure the first `ident'` is `_` or a constructor name. -/ -private def checkAltCtorNames (alts : Array Syntax) (ctorNames : List Name) : TacticM Unit := do +private def checkAltCtorNames (alts : Array Syntax) (ctorNames : List Name) : TacticM Unit := for alt in alts do let n := getAltName alt withRef alt $ trace[Elab.checkAlt]! "{n} , {alt}" diff --git a/stage0/src/Lean/Elab/Tactic/Injection.lean b/stage0/src/Lean/Elab/Tactic/Injection.lean index c98d70d79c..e20e946b4d 100644 --- a/stage0/src/Lean/Elab/Tactic/Injection.lean +++ b/stage0/src/Lean/Elab/Tactic/Injection.lean @@ -14,7 +14,7 @@ private def getInjectionNewIds (stx : Syntax) : List Name := else stx[1].getArgs.toList.map Syntax.getId -private def checkUnusedIds (mvarId : MVarId) (unusedIds : List Name) : MetaM Unit := do +private def checkUnusedIds (mvarId : MVarId) (unusedIds : List Name) : MetaM Unit := unless unusedIds.isEmpty do Meta.throwTacticEx `injection mvarId msg!"too many identifiers provided, unused: {unusedIds}" diff --git a/stage0/src/Lean/Elab/Term.lean b/stage0/src/Lean/Elab/Term.lean index abd54142d7..2dbbbba250 100644 --- a/stage0/src/Lean/Elab/Term.lean +++ b/stage0/src/Lean/Elab/Term.lean @@ -284,8 +284,8 @@ instance : MonadResolveName TermElabM := { def getDeclName? : TermElabM (Option Name) := do pure (← read).declName? def getLetRecsToLift : TermElabM (List LetRecToLift) := do pure (← get).letRecsToLift -def isExprMVarAssigned (mvarId : MVarId) : TermElabM Bool := do return (← getMCtx).isExprAssigned mvarId -def getMVarDecl (mvarId : MVarId) : TermElabM MetavarDecl := do return (← getMCtx).getDecl mvarId +def isExprMVarAssigned (mvarId : MVarId) : TermElabM Bool := return (← getMCtx).isExprAssigned mvarId +def getMVarDecl (mvarId : MVarId) : TermElabM MetavarDecl := return (← getMCtx).getDecl mvarId def assignLevelMVar (mvarId : MVarId) (val : Level) : TermElabM Unit := modifyThe Meta.State fun s => { s with mctx := s.mctx.assignLevel mvarId val } def withDeclName {α} (name : Name) (x : TermElabM α) : TermElabM α := diff --git a/stage0/src/Lean/Meta/AbstractNestedProofs.lean b/stage0/src/Lean/Meta/AbstractNestedProofs.lean index f82ff5c89e..f3b16a656d 100644 --- a/stage0/src/Lean/Meta/AbstractNestedProofs.lean +++ b/stage0/src/Lean/Meta/AbstractNestedProofs.lean @@ -56,7 +56,7 @@ partial def visit (e : Expr) : M Expr := do | Expr.forallE _ _ _ _ => forallTelescope e fun xs b => visitBinders xs do mkForallFVars xs (← visit b) | Expr.mdata _ b _ => return e.updateMData! (← visit b) | Expr.proj _ _ b _ => return e.updateProj! (← visit b) - | Expr.app _ _ _ => e.withApp fun f args => do return mkAppN f (← args.mapM visit) + | Expr.app _ _ _ => e.withApp fun f args => return mkAppN f (← args.mapM visit) | _ => pure e end AbstractNestedProofs diff --git a/stage0/src/Lean/Meta/Closure.lean b/stage0/src/Lean/Meta/Closure.lean index e80981a67d..128951060f 100644 --- a/stage0/src/Lean/Meta/Closure.lean +++ b/stage0/src/Lean/Meta/Closure.lean @@ -154,9 +154,9 @@ def mkNewLevelParam (u : Level) : ClosureM Level := do pure $ mkLevelParam p partial def collectLevelAux : Level → ClosureM Level - | u@(Level.succ v _) => do return u.updateSucc! (← visitLevel collectLevelAux v) - | u@(Level.max v w _) => do return u.updateMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w) - | u@(Level.imax v w _) => do return u.updateIMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w) + | u@(Level.succ v _) => return u.updateSucc! (← visitLevel collectLevelAux v) + | u@(Level.max v w _) => return u.updateMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w) + | u@(Level.imax v w _) => return u.updateIMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w) | u@(Level.mvar mvarId _) => mkNewLevelParam u | u@(Level.param _ _) => mkNewLevelParam u | u@(Level.zero _) => pure u diff --git a/stage0/src/Lean/Meta/RecursorInfo.lean b/stage0/src/Lean/Meta/RecursorInfo.lean index d9759602eb..df8c45d33d 100644 --- a/stage0/src/Lean/Meta/RecursorInfo.lean +++ b/stage0/src/Lean/Meta/RecursorInfo.lean @@ -113,7 +113,7 @@ private def getMajorPosIfAuxRecursor? (declName : Name) (majorPos? : Option Nat) pure $ some (val.nparams + val.nindices + (if s == casesOnSuffix then 1 else val.nmotives)) | _ => pure none -private def checkMotive (declName : Name) (motive : Expr) (motiveArgs : Array Expr) : MetaM Unit := do +private def checkMotive (declName : Name) (motive : Expr) (motiveArgs : Array Expr) : MetaM Unit := unless motive.isFVar && motiveArgs.all Expr.isFVar do throwError! "invalid user defined recursor '{declName}', result type must be of the form (C t), where C is a bound variable, and t is a (possibly empty) sequence of bound variables" diff --git a/stage0/src/Lean/Meta/Tactic/Assumption.lean b/stage0/src/Lean/Meta/Tactic/Assumption.lean index 186596abe6..c38a503875 100644 --- a/stage0/src/Lean/Meta/Tactic/Assumption.lean +++ b/stage0/src/Lean/Meta/Tactic/Assumption.lean @@ -24,7 +24,7 @@ def assumptionAux (mvarId : MVarId) : MetaM Bool := | some h => do assignExprMVar mvarId h; pure true | none => pure false -def assumption (mvarId : MVarId) : MetaM Unit := do +def assumption (mvarId : MVarId) : MetaM Unit := unless (← assumptionAux mvarId) do throwTacticEx `assumption mvarId "" diff --git a/stage0/src/Lean/MetavarContext.lean b/stage0/src/Lean/MetavarContext.lean index 08cc8a6dbf..50e6f414ea 100644 --- a/stage0/src/Lean/MetavarContext.lean +++ b/stage0/src/Lean/MetavarContext.lean @@ -498,9 +498,9 @@ def hasAssignableMVar (mctx : MetavarContext) : Expr → Bool | Expr.localE _ _ _ _ => unreachable! partial def instantiateLevelMVars {m} [Monad m] [MonadMCtx m] : Level → m Level - | lvl@(Level.succ lvl₁ _) => do return Level.updateSucc! lvl (← instantiateLevelMVars lvl₁) - | lvl@(Level.max lvl₁ lvl₂ _) => do return Level.updateMax! lvl (← instantiateLevelMVars lvl₁) (← instantiateLevelMVars lvl₂) - | lvl@(Level.imax lvl₁ lvl₂ _) => do return Level.updateIMax! lvl (← instantiateLevelMVars lvl₁) (← instantiateLevelMVars lvl₂) + | lvl@(Level.succ lvl₁ _) => return Level.updateSucc! lvl (← instantiateLevelMVars lvl₁) + | lvl@(Level.max lvl₁ lvl₂ _) => return Level.updateMax! lvl (← instantiateLevelMVars lvl₁) (← instantiateLevelMVars lvl₂) + | lvl@(Level.imax lvl₁ lvl₂ _) => return Level.updateIMax! lvl (← instantiateLevelMVars lvl₁) (← instantiateLevelMVars lvl₂) | lvl@(Level.mvar mvarId _) => do match getLevelAssignment? (← getMCtx) mvarId with | some newLvl => diff --git a/stage0/stdlib/Lean/Elab/App.c b/stage0/stdlib/Lean/Elab/App.c index 14beccbc60..eabc0dcb55 100644 --- a/stage0/stdlib/Lean/Elab/App.c +++ b/stage0/stdlib/Lean/Elab/App.c @@ -563,7 +563,7 @@ lean_object* l_Lean_Elab_getRefPos___at___private_Lean_Elab_App_0__Lean_Elab_Ter lean_object* l___regBuiltin_Lean_Elab_Term_elabChoice___closed__1; lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_finalize___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_getForallBody___lambda__1___boxed(lean_object*, lean_object*); -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_App___hyg_7434_(lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_App___hyg_7437_(lean_object*); lean_object* l___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppAux(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkForall(lean_object*, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_ElabAppArgs_main_match__1(lean_object*); @@ -36036,7 +36036,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_App___hyg_7434_(lean_object* x_1) { +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_App___hyg_7437_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -36365,7 +36365,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabArrayRef___closed__1); res = l___regBuiltin_Lean_Elab_Term_elabArrayRef(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_App___hyg_7434_(lean_io_mk_world()); +res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_App___hyg_7437_(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)); diff --git a/stage0/stdlib/Lean/Elab/Command.c b/stage0/stdlib/Lean/Elab/Command.c index 6722cd21a1..80b9804730 100644 --- a/stage0/stdlib/Lean/Elab/Command.c +++ b/stage0/stdlib/Lean/Elab/Command.c @@ -143,6 +143,7 @@ extern lean_object* l_Lean_Elab_logException___rarg___lambda__1___closed__3; lean_object* l_Lean_Elab_Command_elabOpen___closed__1; lean_object* l_Lean_Elab_Command_Lean_Elab_Command___instance__1___closed__1; lean_object* lean_private_to_user_name(lean_object*); +lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1147____closed__1; lean_object* l___private_Lean_Elab_Command_0__Lean_Elab_Command_addScopes___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Elab_Command_elabSynth___closed__3; lean_object* l_Lean_Elab_Command_Lean_Elab_Command___instance__2___closed__3; @@ -173,7 +174,6 @@ lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_elabVariable lean_object* l___regBuiltin_Lean_Elab_Command_elabExport___closed__1; lean_object* l_Lean_Elab_Command_elabCheck(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_array_get_size(lean_object*); -lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1146____closed__1; lean_object* l_Lean_Elab_logAt___at_Lean_Elab_Command_logUnknownDecl___spec__2(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*); lean_object* lean_string_append(lean_object*, lean_object*); lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__2___closed__1; @@ -398,8 +398,8 @@ lean_object* l___regBuiltin_Lean_Elab_Command_elbChoice___closed__1; lean_object* l_Std_PersistentArray_foldlM___at___private_Lean_Elab_Command_0__Lean_Elab_Command_addTraceAsMessages___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Elab_Command_elabVariable___closed__1; lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_145_(lean_object*); -lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1146_(lean_object*); -lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_878_(lean_object*); +lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1147_(lean_object*); +lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_879_(lean_object*); lean_object* l_Lean_Elab_Command_elabSetOption_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Syntax_getId(lean_object*); lean_object* l_Lean_Elab_Command_Lean_Elab_Command___instance__11___closed__4; @@ -4545,7 +4545,7 @@ lean_ctor_set(x_3, 1, x_1); return x_3; } } -lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_878_(lean_object* x_1) { +lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_879_(lean_object* x_1) { _start: { lean_object* x_2; @@ -5490,7 +5490,7 @@ return x_65; } } } -static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1146____closed__1() { +static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1147____closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -5500,11 +5500,11 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1146_(lean_object* x_1) { +lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1147_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; -x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1146____closed__1; +x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1147____closed__1; x_3 = l_Lean_registerTraceClass(x_2, x_1); return x_3; } @@ -6192,7 +6192,7 @@ lean_dec(x_128); x_130 = lean_ctor_get(x_129, 2); lean_inc(x_130); lean_dec(x_129); -x_131 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1146____closed__1; +x_131 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1147____closed__1; x_132 = l_Lean_checkTraceOption(x_130, x_131); lean_dec(x_130); if (x_132 == 0) @@ -6301,7 +6301,7 @@ lean_dec(x_154); x_156 = lean_ctor_get(x_155, 2); lean_inc(x_156); lean_dec(x_155); -x_157 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1146____closed__1; +x_157 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1147____closed__1; x_158 = l_Lean_checkTraceOption(x_156, x_157); lean_dec(x_156); if (x_158 == 0) @@ -6857,7 +6857,7 @@ lean_dec(x_290); x_292 = lean_ctor_get(x_291, 2); lean_inc(x_292); lean_dec(x_291); -x_293 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1146____closed__1; +x_293 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1147____closed__1; x_294 = l_Lean_checkTraceOption(x_292, x_293); lean_dec(x_292); if (x_294 == 0) @@ -7458,7 +7458,7 @@ lean_dec(x_436); x_438 = lean_ctor_get(x_437, 2); lean_inc(x_438); lean_dec(x_437); -x_439 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1146____closed__1; +x_439 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1147____closed__1; x_440 = l_Lean_checkTraceOption(x_438, x_439); lean_dec(x_438); if (x_440 == 0) @@ -23079,7 +23079,7 @@ l_Lean_Elab_Command_mkCommandElabAttributeUnsafe___closed__8 = _init_l_Lean_Elab lean_mark_persistent(l_Lean_Elab_Command_mkCommandElabAttributeUnsafe___closed__8); l_Lean_Elab_Command_mkCommandElabAttributeUnsafe___closed__9 = _init_l_Lean_Elab_Command_mkCommandElabAttributeUnsafe___closed__9(); lean_mark_persistent(l_Lean_Elab_Command_mkCommandElabAttributeUnsafe___closed__9); -res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_878_(lean_io_mk_world()); +res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_879_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_Elab_Command_commandElabAttribute = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_Elab_Command_commandElabAttribute); @@ -23112,9 +23112,9 @@ l_Lean_Elab_Command_withLogging___closed__1 = _init_l_Lean_Elab_Command_withLogg lean_mark_persistent(l_Lean_Elab_Command_withLogging___closed__1); l_Lean_Elab_Command_withLogging___closed__2 = _init_l_Lean_Elab_Command_withLogging___closed__2(); lean_mark_persistent(l_Lean_Elab_Command_withLogging___closed__2); -l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1146____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1146____closed__1(); -lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1146____closed__1); -res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1146_(lean_io_mk_world()); +l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1147____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1147____closed__1(); +lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1147____closed__1); +res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_Command___hyg_1147_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); l_Lean_Elab_Command_elabCommand___lambda__1___closed__1 = _init_l_Lean_Elab_Command_elabCommand___lambda__1___closed__1(); diff --git a/stage0/stdlib/Lean/Elab/Do.c b/stage0/stdlib/Lean/Elab/Do.c index 5ff0373c80..292b7c1fe0 100644 --- a/stage0/stdlib/Lean/Elab/Do.c +++ b/stage0/stdlib/Lean/Elab/Do.c @@ -448,6 +448,7 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTermCore___closed__10; uint8_t l_Array_anyMUnsafe_any___at_Lean_Elab_Term_Do_ToCodeBlock_tryCatchPred___spec__1(lean_object*, lean_object*, size_t, size_t); lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_ensureInsideFor(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__1; lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTermCore___closed__1; lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Syntax_copyInfo(lean_object*, lean_object*); @@ -576,7 +577,6 @@ lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_ToCodeBlo lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_Do_ToCodeBlock_doMatchToCode___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Term_Do_hasBreakContinueReturn___spec__2___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_expandOptType(lean_object*, lean_object*); -extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__1; lean_object* l_Lean_Elab_Term_Do_CodeBlocl_toMessageData_loop___closed__6; lean_object* l_Array_foldrMUnsafe_fold___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkTuple___spec__1___closed__1; lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_Do_ToTerm_mkJoinPointCore___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -728,7 +728,7 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTerm___boxed(lean_object*, lean_ lean_object* l_Lean_Elab_Term_Do_pullExitPointsAux___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_foldrMUnsafe_fold___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_expandDoIf_x3f___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*); lean_object* l_Lean_Elab_Term_Do_hasExitPointPred_loop___at_Lean_Elab_Term_Do_hasTerminalAction___spec__1___boxed(lean_object*); -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_23284_(lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_23285_(lean_object*); lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_ensureEOS___closed__3; lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode___closed__3; lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doReassignArrowToCode___closed__3; @@ -25477,7 +25477,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_mkAppStx___closed__6; -x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__1; +x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } @@ -46830,7 +46830,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_23284_(lean_object* x_1) { +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_23285_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -47928,7 +47928,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_Do_elabDo___closed__1); res = l___regBuiltin_Lean_Elab_Term_Do_elabDo(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_23284_(lean_io_mk_world()); +res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Do___hyg_23285_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); l___regBuiltin_Lean_Elab_Term_expandTermFor___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_expandTermFor___closed__1(); diff --git a/stage0/stdlib/Lean/Elab/LetRec.c b/stage0/stdlib/Lean/Elab/LetRec.c index 368bcc7fd2..868e753b02 100644 --- a/stage0/stdlib/Lean/Elab/LetRec.c +++ b/stage0/stdlib/Lean/Elab/LetRec.c @@ -78,6 +78,7 @@ lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_LetRec_0__Lean_El lean_object* l___private_Lean_Elab_LetRec_0__Lean_Elab_Term_withAuxLocalDecls___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__1; lean_object* l_Array_mapIdxM_map___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_registerLetRecsToLift___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_replaceRef(lean_object*, lean_object*); lean_object* lean_array_get(lean_object*, lean_object*, lean_object*); @@ -102,7 +103,6 @@ lean_object* l_Lean_throwErrorAt___at___private_Lean_Elab_Term_0__Lean_Elab_Term lean_object* l_Lean_Elab_Term_getCurrMacroScope(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Environment_contains(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_expandOptType(lean_object*, lean_object*); -extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__1; extern lean_object* l_Lean_mkAppStx___closed__6; lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__7___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__7___lambda__3___closed__1; @@ -2690,7 +2690,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_mkAppStx___closed__6; -x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__1; +x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } diff --git a/stage0/stdlib/Lean/Elab/StructInst.c b/stage0/stdlib/Lean/Elab/StructInst.c index 49438e4948..13fb986c06 100644 --- a/stage0/stdlib/Lean/Elab/StructInst.c +++ b/stage0/stdlib/Lean/Elab/StructInst.c @@ -48,7 +48,6 @@ extern lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_953____closed__7 lean_object* l_Lean_Meta_getExprMVarAssignment_x3f___at___private_Lean_Meta_Basic_0__Lean_Meta_isClassQuick_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_lambdaLetTelescope___at___private_Lean_Meta_InferType_0__Lean_Meta_inferLambdaType___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_StructInst_DefaultFields_reduce___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1; lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_isModifyOp_x3f___spec__1___closed__7; lean_object* l_Lean_Elab_Term_StructInst_Struct_allDefault_match__2___rarg(lean_object*, lean_object*); extern lean_object* l_Lean_nullKind; @@ -78,25 +77,26 @@ lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_getFi lean_object* l_Lean_Elab_Term_StructInst_Lean_Elab_StructInst___instance__5; lean_object* l_Std_AssocList_foldlM___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkFieldMap___spec__7(lean_object*, lean_object*); uint8_t l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_getFieldIdx___lambda__1(lean_object*, lean_object*); -lean_object* l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__2; extern lean_object* l_Lean_Init_LeanInit___instance__9; lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandNumLitFields_match__1(lean_object*); lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_reduce_match__3(lean_object*); lean_object* l_Lean_Elab_Term_StructInst_formatStruct_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Macros___hyg_464____closed__2; extern lean_object* l_Array_myMacro____x40_Init_Data_Array_Macros___hyg_464____closed__8; +lean_object* l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__2; extern lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_expandApp___spec__1___closed__1; lean_object* l_Lean_Elab_Term_StructInst_Lean_Elab_StructInst___instance__4(lean_object*); lean_object* lean_array_uset(lean_object*, size_t, lean_object*); lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkProjStx(lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Elab_Term_StructInst_elabStructInst___closed__1; lean_object* l_Lean_Elab_Term_StructInst_throwFailedToElabField___rarg___closed__3; -lean_object* l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___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* l_Lean_Elab_Term_StructInst_Lean_Elab_StructInst___instance__2; lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandNumLitFields___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_StructInst_elabStructInst_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_reduce___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Format_joinSep___at_Lean_Elab_Term_StructInst_formatField___spec__1(lean_object*, lean_object*); +lean_object* l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1; lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStructInstAux_match__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_getFieldValue_x3f(lean_object*, lean_object*); extern lean_object* l_Lean_myMacro____x40_Lean_Data_FormatMacro___hyg_38____closed__2; @@ -112,7 +112,7 @@ extern lean_object* l_Array_empty___closed__1; lean_object* lean_environment_find(lean_object*, lean_object*); lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_getStructName___rarg___closed__5; lean_object* l_Lean_Elab_Term_StructInst_Lean_Elab_StructInst___instance__8; -lean_object* l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_6252_(lean_object*); +lean_object* l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_6337_(lean_object*); lean_object* l_List_foldlM___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkFieldMap___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValueAux_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_isModifyOp_x3f___spec__1___closed__5; @@ -384,7 +384,6 @@ uint8_t l_Lean_Expr_isAppOfArity(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop_match__3___rarg(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandParentFields_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* lean_expr_dbg_to_string(lean_object*); -lean_object* l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_mapM___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkCtorHeader___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__2; lean_object* l_Lean_Elab_Term_StructInst_defaultMissing_x3f(lean_object*); @@ -428,7 +427,6 @@ lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_isMod lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkCtorHeaderAux___closed__2; lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_isModifyOp_x3f___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Elab_Term_StructInst_Field_isSimple___rarg(lean_object*); -lean_object* l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___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* l_List_map___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandCompositeFields___spec__3(lean_object*); lean_object* l___private_Lean_Meta_SynthInstance_0__Lean_Meta_synthInstanceImp_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_StructInst_Struct_fields(lean_object*); @@ -487,6 +485,7 @@ uint8_t l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___ lean_object* l_Lean_Elab_Term_StructInst_findField_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Expr_FindImpl_initCache; lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_reduce_match__3___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabModifyOp___closed__4; extern lean_object* l_Lean_Meta_substCore___lambda__13___closed__25; lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_step_match__1(lean_object*); @@ -597,6 +596,7 @@ lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_getSt lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_groupFields___lambda__2___closed__2; lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*); extern lean_object* l_Id_Init_Control_Id___instance__1; +extern lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1; uint8_t l_Lean_Syntax_isNone(lean_object*); lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandNonAtomicExplicitSource___closed__3; lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_propagateExpectedType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -616,6 +616,7 @@ lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValue_x3f(lean_o lean_object* l_Lean_isSubobjectField_x3f(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_isSimpleField_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStructInstAux___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_mk_array(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_StructInst_Struct_modifyFieldsM___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_StructInst_setStructSourceSyntax_match__1(lean_object*); @@ -648,7 +649,6 @@ lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_toFie lean_object* l_Std_HashMapImp_find_x3f___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkFieldMap___spec__1___boxed(lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_reduce_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Format_joinSep___at___private_Lean_Data_Trie_0__Lean_Parser_Trie_toStringAux___spec__1(lean_object*, lean_object*); -lean_object* l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStruct_match__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_mkFreshLevelMVar___at_Lean_Elab_Term_ensureType___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*); @@ -24892,7 +24892,7 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_StructInst_DefaultFields_step_ return x_2; } } -static lean_object* _init_l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1() { +static lean_object* _init_l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1() { _start: { lean_object* x_1; @@ -24900,20 +24900,20 @@ x_1 = lean_mk_string("Lean.Elab.Term.StructInst.DefaultFields.step"); return x_1; } } -static lean_object* _init_l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__2() { +static lean_object* _init_l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__2() { _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_Elab_StructInst_0__Lean_Elab_Term_StructInst_getStructSource___closed__4; -x_2 = l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1; -x_3 = lean_unsigned_to_nat(721u); -x_4 = lean_unsigned_to_nat(23u); +x_2 = l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1; +x_3 = lean_unsigned_to_nat(722u); +x_4 = lean_unsigned_to_nat(25u); x_5 = l___private_Init_LeanInit_0__Lean_eraseMacroScopesAux___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); return x_6; } } -lean_object* l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1(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) { +lean_object* l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1(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; @@ -24928,39 +24928,133 @@ x_13 = lean_ctor_get(x_12, 0); lean_inc(x_13); lean_dec(x_12); x_14 = l_Lean_Elab_Term_StructInst_DefaultFields_step(x_13, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11); +if (lean_obj_tag(x_14) == 0) +{ +uint8_t x_15; +x_15 = !lean_is_exclusive(x_14); +if (x_15 == 0) +{ +lean_object* x_16; lean_object* x_17; +x_16 = lean_ctor_get(x_14, 0); +lean_dec(x_16); +x_17 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1; +lean_ctor_set(x_14, 0, x_17); return x_14; } else { -lean_object* x_15; -lean_dec(x_12); -x_15 = lean_ctor_get(x_1, 3); -lean_inc(x_15); -if (lean_obj_tag(x_15) == 0) -{ -lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; -lean_dec(x_1); -x_16 = l_Init_Core___instance__49; -x_17 = l_Init_Control_Monad___instance__2___rarg(x_2, x_16); -x_18 = lean_alloc_closure((void*)(l_Init_Control_Reader___instance__1___rarg___boxed), 2, 1); -lean_closure_set(x_18, 0, x_17); -x_19 = l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__2; -x_20 = lean_panic_fn(x_18, x_19); -x_21 = lean_apply_9(x_20, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11); -return x_21; +lean_object* x_18; lean_object* x_19; lean_object* x_20; +x_18 = lean_ctor_get(x_14, 1); +lean_inc(x_18); +lean_dec(x_14); +x_19 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1; +x_20 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_20, 0, x_19); +lean_ctor_set(x_20, 1, x_18); +return x_20; +} } else { -lean_object* x_22; lean_object* x_23; -lean_dec(x_2); -x_22 = lean_ctor_get(x_15, 0); -lean_inc(x_22); -lean_dec(x_15); -x_23 = l_Lean_Elab_Term_StructInst_defaultMissing_x3f(x_22); -lean_dec(x_22); -if (lean_obj_tag(x_23) == 0) +uint8_t x_21; +x_21 = !lean_is_exclusive(x_14); +if (x_21 == 0) { -lean_object* x_24; lean_object* x_25; +return x_14; +} +else +{ +lean_object* x_22; lean_object* x_23; lean_object* x_24; +x_22 = lean_ctor_get(x_14, 0); +x_23 = lean_ctor_get(x_14, 1); +lean_inc(x_23); +lean_inc(x_22); +lean_dec(x_14); +x_24 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_24, 0, x_22); +lean_ctor_set(x_24, 1, x_23); +return x_24; +} +} +} +else +{ +lean_object* x_25; +lean_dec(x_12); +x_25 = lean_ctor_get(x_1, 3); +lean_inc(x_25); +if (lean_obj_tag(x_25) == 0) +{ +lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; +lean_dec(x_1); +x_26 = l_Init_Core___instance__49; +x_27 = l_Init_Control_Monad___instance__2___rarg(x_2, x_26); +x_28 = lean_alloc_closure((void*)(l_Init_Control_Reader___instance__1___rarg___boxed), 2, 1); +lean_closure_set(x_28, 0, x_27); +x_29 = l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__2; +x_30 = lean_panic_fn(x_28, x_29); +x_31 = lean_apply_9(x_30, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11); +if (lean_obj_tag(x_31) == 0) +{ +uint8_t x_32; +x_32 = !lean_is_exclusive(x_31); +if (x_32 == 0) +{ +lean_object* x_33; lean_object* x_34; +x_33 = lean_ctor_get(x_31, 0); +lean_dec(x_33); +x_34 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1; +lean_ctor_set(x_31, 0, x_34); +return x_31; +} +else +{ +lean_object* x_35; lean_object* x_36; lean_object* x_37; +x_35 = lean_ctor_get(x_31, 1); +lean_inc(x_35); +lean_dec(x_31); +x_36 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1; +x_37 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_37, 0, x_36); +lean_ctor_set(x_37, 1, x_35); +return x_37; +} +} +else +{ +uint8_t x_38; +x_38 = !lean_is_exclusive(x_31); +if (x_38 == 0) +{ +return x_31; +} +else +{ +lean_object* x_39; lean_object* x_40; lean_object* x_41; +x_39 = lean_ctor_get(x_31, 0); +x_40 = lean_ctor_get(x_31, 1); +lean_inc(x_40); +lean_inc(x_39); +lean_dec(x_31); +x_41 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_41, 0, x_39); +lean_ctor_set(x_41, 1, x_40); +return x_41; +} +} +} +else +{ +lean_object* x_42; lean_object* x_43; +lean_dec(x_2); +x_42 = lean_ctor_get(x_25, 0); +lean_inc(x_42); +lean_dec(x_25); +x_43 = l_Lean_Elab_Term_StructInst_defaultMissing_x3f(x_42); +lean_dec(x_42); +if (lean_obj_tag(x_43) == 0) +{ +lean_object* x_44; lean_object* x_45; lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); @@ -24970,314 +25064,277 @@ lean_dec(x_5); lean_dec(x_4); lean_dec(x_3); lean_dec(x_1); -x_24 = lean_box(0); -x_25 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_25, 0, x_24); -lean_ctor_set(x_25, 1, x_11); -return x_25; +x_44 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1; +x_45 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_45, 0, x_44); +lean_ctor_set(x_45, 1, x_11); +return x_45; } else { -lean_object* x_26; -x_26 = lean_ctor_get(x_23, 0); -lean_inc(x_26); -lean_dec(x_23); -if (lean_obj_tag(x_26) == 2) +lean_object* x_46; +x_46 = lean_ctor_get(x_43, 0); +lean_inc(x_46); +lean_dec(x_43); +if (lean_obj_tag(x_46) == 2) { -lean_object* x_27; lean_object* x_28; lean_object* x_29; uint8_t x_30; -x_27 = lean_ctor_get(x_26, 0); -lean_inc(x_27); -lean_dec(x_26); -lean_inc(x_27); -x_28 = l_Lean_Elab_Term_isExprMVarAssigned(x_27, x_5, x_6, x_7, x_8, x_9, x_10, x_11); -x_29 = lean_ctor_get(x_28, 0); -lean_inc(x_29); -x_30 = lean_unbox(x_29); -lean_dec(x_29); -if (x_30 == 0) -{ -lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; uint8_t x_37; -x_31 = lean_ctor_get(x_28, 1); -lean_inc(x_31); -lean_dec(x_28); -x_32 = lean_ctor_get(x_1, 0); -lean_inc(x_32); -x_33 = lean_ctor_get(x_3, 0); -lean_inc(x_33); -x_34 = lean_ctor_get(x_3, 1); -lean_inc(x_34); -x_35 = lean_ctor_get(x_3, 2); -lean_inc(x_35); -lean_dec(x_3); -x_36 = l_Lean_Elab_Term_StructInst_DefaultFields_getFieldName(x_1); -lean_dec(x_1); -x_37 = !lean_is_exclusive(x_9); -if (x_37 == 0) -{ -lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; -x_38 = lean_ctor_get(x_9, 3); -x_39 = l_Lean_replaceRef(x_32, x_38); -lean_dec(x_38); -lean_dec(x_32); -lean_ctor_set(x_9, 3, x_39); -x_40 = lean_unsigned_to_nat(0u); -x_41 = l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop(x_33, x_34, x_35, x_36, x_27, x_40, x_40, x_5, x_6, x_7, x_8, x_9, x_10, x_31); -lean_dec(x_35); -lean_dec(x_33); -if (lean_obj_tag(x_41) == 0) -{ -lean_object* x_42; uint8_t x_43; -x_42 = lean_ctor_get(x_41, 0); -lean_inc(x_42); -x_43 = lean_unbox(x_42); -lean_dec(x_42); -if (x_43 == 0) -{ -uint8_t x_44; -lean_dec(x_4); -x_44 = !lean_is_exclusive(x_41); -if (x_44 == 0) -{ -lean_object* x_45; lean_object* x_46; -x_45 = lean_ctor_get(x_41, 0); -lean_dec(x_45); -x_46 = lean_box(0); -lean_ctor_set(x_41, 0, x_46); -return x_41; -} -else -{ -lean_object* x_47; lean_object* x_48; lean_object* x_49; -x_47 = lean_ctor_get(x_41, 1); +lean_object* x_47; lean_object* x_48; lean_object* x_49; uint8_t x_50; +x_47 = lean_ctor_get(x_46, 0); lean_inc(x_47); -lean_dec(x_41); -x_48 = lean_box(0); -x_49 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_49, 0, x_48); -lean_ctor_set(x_49, 1, x_47); -return x_49; -} -} -else +lean_dec(x_46); +lean_inc(x_47); +x_48 = l_Lean_Elab_Term_isExprMVarAssigned(x_47, x_5, x_6, x_7, x_8, x_9, x_10, x_11); +x_49 = lean_ctor_get(x_48, 0); +lean_inc(x_49); +x_50 = lean_unbox(x_49); +lean_dec(x_49); +if (x_50 == 0) { -lean_object* x_50; lean_object* x_51; lean_object* x_52; uint8_t x_53; lean_object* x_54; lean_object* x_55; uint8_t x_56; -x_50 = lean_ctor_get(x_41, 1); -lean_inc(x_50); -lean_dec(x_41); -x_51 = lean_st_ref_take(x_4, x_50); -x_52 = lean_ctor_get(x_51, 1); +lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; uint8_t x_57; +x_51 = lean_ctor_get(x_48, 1); +lean_inc(x_51); +lean_dec(x_48); +x_52 = lean_ctor_get(x_1, 0); lean_inc(x_52); -lean_dec(x_51); -x_53 = 1; -x_54 = lean_box(x_53); -x_55 = lean_st_ref_set(x_4, x_54, x_52); -lean_dec(x_4); -x_56 = !lean_is_exclusive(x_55); -if (x_56 == 0) +x_53 = lean_ctor_get(x_3, 0); +lean_inc(x_53); +x_54 = lean_ctor_get(x_3, 1); +lean_inc(x_54); +x_55 = lean_ctor_get(x_3, 2); +lean_inc(x_55); +lean_dec(x_3); +x_56 = l_Lean_Elab_Term_StructInst_DefaultFields_getFieldName(x_1); +lean_dec(x_1); +x_57 = !lean_is_exclusive(x_9); +if (x_57 == 0) { -lean_object* x_57; lean_object* x_58; -x_57 = lean_ctor_get(x_55, 0); -lean_dec(x_57); -x_58 = lean_box(0); -lean_ctor_set(x_55, 0, x_58); -return x_55; -} -else -{ -lean_object* x_59; lean_object* x_60; lean_object* x_61; -x_59 = lean_ctor_get(x_55, 1); -lean_inc(x_59); +lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; +x_58 = lean_ctor_get(x_9, 3); +x_59 = l_Lean_replaceRef(x_52, x_58); +lean_dec(x_58); +lean_dec(x_52); +lean_ctor_set(x_9, 3, x_59); +x_60 = lean_unsigned_to_nat(0u); +x_61 = l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop(x_53, x_54, x_55, x_56, x_47, x_60, x_60, x_5, x_6, x_7, x_8, x_9, x_10, x_51); lean_dec(x_55); -x_60 = lean_box(0); -x_61 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_61, 0, x_60); -lean_ctor_set(x_61, 1, x_59); +lean_dec(x_53); +if (lean_obj_tag(x_61) == 0) +{ +lean_object* x_62; uint8_t x_63; +x_62 = lean_ctor_get(x_61, 0); +lean_inc(x_62); +x_63 = lean_unbox(x_62); +lean_dec(x_62); +if (x_63 == 0) +{ +uint8_t x_64; +lean_dec(x_4); +x_64 = !lean_is_exclusive(x_61); +if (x_64 == 0) +{ +lean_object* x_65; lean_object* x_66; +x_65 = lean_ctor_get(x_61, 0); +lean_dec(x_65); +x_66 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1; +lean_ctor_set(x_61, 0, x_66); return x_61; } -} -} else { -uint8_t x_62; -lean_dec(x_4); -x_62 = !lean_is_exclusive(x_41); -if (x_62 == 0) -{ -return x_41; -} -else -{ -lean_object* x_63; lean_object* x_64; lean_object* x_65; -x_63 = lean_ctor_get(x_41, 0); -x_64 = lean_ctor_get(x_41, 1); -lean_inc(x_64); -lean_inc(x_63); -lean_dec(x_41); -x_65 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_65, 0, x_63); -lean_ctor_set(x_65, 1, x_64); -return x_65; -} -} -} -else -{ -lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; -x_66 = lean_ctor_get(x_9, 0); -x_67 = lean_ctor_get(x_9, 1); -x_68 = lean_ctor_get(x_9, 2); -x_69 = lean_ctor_get(x_9, 3); -lean_inc(x_69); -lean_inc(x_68); +lean_object* x_67; lean_object* x_68; lean_object* x_69; +x_67 = lean_ctor_get(x_61, 1); lean_inc(x_67); -lean_inc(x_66); -lean_dec(x_9); -x_70 = l_Lean_replaceRef(x_32, x_69); -lean_dec(x_69); -lean_dec(x_32); -x_71 = lean_alloc_ctor(0, 4, 0); -lean_ctor_set(x_71, 0, x_66); -lean_ctor_set(x_71, 1, x_67); -lean_ctor_set(x_71, 2, x_68); -lean_ctor_set(x_71, 3, x_70); -x_72 = lean_unsigned_to_nat(0u); -x_73 = l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop(x_33, x_34, x_35, x_36, x_27, x_72, x_72, x_5, x_6, x_7, x_8, x_71, x_10, x_31); -lean_dec(x_35); -lean_dec(x_33); -if (lean_obj_tag(x_73) == 0) -{ -lean_object* x_74; uint8_t x_75; -x_74 = lean_ctor_get(x_73, 0); -lean_inc(x_74); -x_75 = lean_unbox(x_74); -lean_dec(x_74); -if (x_75 == 0) -{ -lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; -lean_dec(x_4); -x_76 = lean_ctor_get(x_73, 1); -lean_inc(x_76); -if (lean_is_exclusive(x_73)) { - lean_ctor_release(x_73, 0); - lean_ctor_release(x_73, 1); - x_77 = x_73; -} else { - lean_dec_ref(x_73); - x_77 = lean_box(0); +lean_dec(x_61); +x_68 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1; +x_69 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_69, 0, x_68); +lean_ctor_set(x_69, 1, x_67); +return x_69; } -x_78 = lean_box(0); -if (lean_is_scalar(x_77)) { - x_79 = lean_alloc_ctor(0, 2, 0); -} else { - x_79 = x_77; -} -lean_ctor_set(x_79, 0, x_78); -lean_ctor_set(x_79, 1, x_76); -return x_79; } else { -lean_object* x_80; lean_object* x_81; lean_object* x_82; uint8_t x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; -x_80 = lean_ctor_get(x_73, 1); -lean_inc(x_80); -lean_dec(x_73); -x_81 = lean_st_ref_take(x_4, x_80); -x_82 = lean_ctor_get(x_81, 1); -lean_inc(x_82); -lean_dec(x_81); -x_83 = 1; -x_84 = lean_box(x_83); -x_85 = lean_st_ref_set(x_4, x_84, x_82); +lean_object* x_70; lean_object* x_71; lean_object* x_72; uint8_t x_73; lean_object* x_74; lean_object* x_75; uint8_t x_76; +x_70 = lean_ctor_get(x_61, 1); +lean_inc(x_70); +lean_dec(x_61); +x_71 = lean_st_ref_take(x_4, x_70); +x_72 = lean_ctor_get(x_71, 1); +lean_inc(x_72); +lean_dec(x_71); +x_73 = 1; +x_74 = lean_box(x_73); +x_75 = lean_st_ref_set(x_4, x_74, x_72); lean_dec(x_4); -x_86 = lean_ctor_get(x_85, 1); +x_76 = !lean_is_exclusive(x_75); +if (x_76 == 0) +{ +lean_object* x_77; lean_object* x_78; +x_77 = lean_ctor_get(x_75, 0); +lean_dec(x_77); +x_78 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1; +lean_ctor_set(x_75, 0, x_78); +return x_75; +} +else +{ +lean_object* x_79; lean_object* x_80; lean_object* x_81; +x_79 = lean_ctor_get(x_75, 1); +lean_inc(x_79); +lean_dec(x_75); +x_80 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1; +x_81 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_81, 0, x_80); +lean_ctor_set(x_81, 1, x_79); +return x_81; +} +} +} +else +{ +uint8_t x_82; +lean_dec(x_4); +x_82 = !lean_is_exclusive(x_61); +if (x_82 == 0) +{ +return x_61; +} +else +{ +lean_object* x_83; lean_object* x_84; lean_object* x_85; +x_83 = lean_ctor_get(x_61, 0); +x_84 = lean_ctor_get(x_61, 1); +lean_inc(x_84); +lean_inc(x_83); +lean_dec(x_61); +x_85 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_85, 0, x_83); +lean_ctor_set(x_85, 1, x_84); +return x_85; +} +} +} +else +{ +lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; +x_86 = lean_ctor_get(x_9, 0); +x_87 = lean_ctor_get(x_9, 1); +x_88 = lean_ctor_get(x_9, 2); +x_89 = lean_ctor_get(x_9, 3); +lean_inc(x_89); +lean_inc(x_88); +lean_inc(x_87); lean_inc(x_86); -if (lean_is_exclusive(x_85)) { - lean_ctor_release(x_85, 0); - lean_ctor_release(x_85, 1); - x_87 = x_85; -} else { - lean_dec_ref(x_85); - x_87 = lean_box(0); -} -x_88 = lean_box(0); -if (lean_is_scalar(x_87)) { - x_89 = lean_alloc_ctor(0, 2, 0); -} else { - x_89 = x_87; -} -lean_ctor_set(x_89, 0, x_88); -lean_ctor_set(x_89, 1, x_86); -return x_89; -} -} -else -{ -lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; -lean_dec(x_4); -x_90 = lean_ctor_get(x_73, 0); -lean_inc(x_90); -x_91 = lean_ctor_get(x_73, 1); -lean_inc(x_91); -if (lean_is_exclusive(x_73)) { - lean_ctor_release(x_73, 0); - lean_ctor_release(x_73, 1); - x_92 = x_73; -} else { - lean_dec_ref(x_73); - x_92 = lean_box(0); -} -if (lean_is_scalar(x_92)) { - x_93 = lean_alloc_ctor(1, 2, 0); -} else { - x_93 = x_92; -} -lean_ctor_set(x_93, 0, x_90); -lean_ctor_set(x_93, 1, x_91); -return x_93; -} -} -} -else -{ -uint8_t x_94; -lean_dec(x_27); -lean_dec(x_10); lean_dec(x_9); -lean_dec(x_8); -lean_dec(x_7); -lean_dec(x_6); -lean_dec(x_5); +x_90 = l_Lean_replaceRef(x_52, x_89); +lean_dec(x_89); +lean_dec(x_52); +x_91 = lean_alloc_ctor(0, 4, 0); +lean_ctor_set(x_91, 0, x_86); +lean_ctor_set(x_91, 1, x_87); +lean_ctor_set(x_91, 2, x_88); +lean_ctor_set(x_91, 3, x_90); +x_92 = lean_unsigned_to_nat(0u); +x_93 = l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop(x_53, x_54, x_55, x_56, x_47, x_92, x_92, x_5, x_6, x_7, x_8, x_91, x_10, x_51); +lean_dec(x_55); +lean_dec(x_53); +if (lean_obj_tag(x_93) == 0) +{ +lean_object* x_94; uint8_t x_95; +x_94 = lean_ctor_get(x_93, 0); +lean_inc(x_94); +x_95 = lean_unbox(x_94); +lean_dec(x_94); +if (x_95 == 0) +{ +lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_dec(x_4); -lean_dec(x_3); -lean_dec(x_1); -x_94 = !lean_is_exclusive(x_28); -if (x_94 == 0) -{ -lean_object* x_95; lean_object* x_96; -x_95 = lean_ctor_get(x_28, 0); -lean_dec(x_95); -x_96 = lean_box(0); -lean_ctor_set(x_28, 0, x_96); -return x_28; +x_96 = lean_ctor_get(x_93, 1); +lean_inc(x_96); +if (lean_is_exclusive(x_93)) { + lean_ctor_release(x_93, 0); + lean_ctor_release(x_93, 1); + x_97 = x_93; +} else { + lean_dec_ref(x_93); + x_97 = lean_box(0); +} +x_98 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1; +if (lean_is_scalar(x_97)) { + x_99 = lean_alloc_ctor(0, 2, 0); +} else { + x_99 = x_97; } -else -{ -lean_object* x_97; lean_object* x_98; lean_object* x_99; -x_97 = lean_ctor_get(x_28, 1); -lean_inc(x_97); -lean_dec(x_28); -x_98 = lean_box(0); -x_99 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_99, 0, x_98); -lean_ctor_set(x_99, 1, x_97); +lean_ctor_set(x_99, 1, x_96); return x_99; } +else +{ +lean_object* x_100; lean_object* x_101; lean_object* x_102; uint8_t x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109; +x_100 = lean_ctor_get(x_93, 1); +lean_inc(x_100); +lean_dec(x_93); +x_101 = lean_st_ref_take(x_4, x_100); +x_102 = lean_ctor_get(x_101, 1); +lean_inc(x_102); +lean_dec(x_101); +x_103 = 1; +x_104 = lean_box(x_103); +x_105 = lean_st_ref_set(x_4, x_104, x_102); +lean_dec(x_4); +x_106 = lean_ctor_get(x_105, 1); +lean_inc(x_106); +if (lean_is_exclusive(x_105)) { + lean_ctor_release(x_105, 0); + lean_ctor_release(x_105, 1); + x_107 = x_105; +} else { + lean_dec_ref(x_105); + x_107 = lean_box(0); +} +x_108 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1; +if (lean_is_scalar(x_107)) { + x_109 = lean_alloc_ctor(0, 2, 0); +} else { + x_109 = x_107; +} +lean_ctor_set(x_109, 0, x_108); +lean_ctor_set(x_109, 1, x_106); +return x_109; } } else { -lean_object* x_100; lean_object* x_101; -lean_dec(x_26); +lean_object* x_110; lean_object* x_111; lean_object* x_112; lean_object* x_113; +lean_dec(x_4); +x_110 = lean_ctor_get(x_93, 0); +lean_inc(x_110); +x_111 = lean_ctor_get(x_93, 1); +lean_inc(x_111); +if (lean_is_exclusive(x_93)) { + lean_ctor_release(x_93, 0); + lean_ctor_release(x_93, 1); + x_112 = x_93; +} else { + lean_dec_ref(x_93); + x_112 = lean_box(0); +} +if (lean_is_scalar(x_112)) { + x_113 = lean_alloc_ctor(1, 2, 0); +} else { + x_113 = x_112; +} +lean_ctor_set(x_113, 0, x_110); +lean_ctor_set(x_113, 1, x_111); +return x_113; +} +} +} +else +{ +uint8_t x_114; +lean_dec(x_47); lean_dec(x_10); lean_dec(x_9); lean_dec(x_8); @@ -25287,45 +25344,105 @@ lean_dec(x_5); lean_dec(x_4); lean_dec(x_3); lean_dec(x_1); -x_100 = lean_box(0); -x_101 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_101, 0, x_100); -lean_ctor_set(x_101, 1, x_11); -return x_101; +x_114 = !lean_is_exclusive(x_48); +if (x_114 == 0) +{ +lean_object* x_115; lean_object* x_116; +x_115 = lean_ctor_get(x_48, 0); +lean_dec(x_115); +x_116 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1; +lean_ctor_set(x_48, 0, x_116); +return x_48; +} +else +{ +lean_object* x_117; lean_object* x_118; lean_object* x_119; +x_117 = lean_ctor_get(x_48, 1); +lean_inc(x_117); +lean_dec(x_48); +x_118 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1; +x_119 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_119, 0, x_118); +lean_ctor_set(x_119, 1, x_117); +return x_119; +} +} +} +else +{ +lean_object* x_120; lean_object* x_121; +lean_dec(x_46); +lean_dec(x_10); +lean_dec(x_9); +lean_dec(x_8); +lean_dec(x_7); +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_1); +x_120 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_applyAttributesCore___spec__1___closed__1; +x_121 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_121, 0, x_120); +lean_ctor_set(x_121, 1, x_11); +return x_121; } } } } } } -lean_object* l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__2(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, lean_object* x_12) { +lean_object* l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__2(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, lean_object* x_12) { _start: { -lean_object* x_13; -x_13 = l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1(x_1, x_2, x_3, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); -return x_13; +if (lean_obj_tag(x_4) == 0) +{ +lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; +lean_dec(x_3); +lean_dec(x_2); +x_13 = lean_ctor_get(x_4, 0); +lean_inc(x_13); +lean_dec(x_4); +x_14 = lean_ctor_get(x_1, 0); +lean_inc(x_14); +lean_dec(x_1); +x_15 = lean_ctor_get(x_14, 1); +lean_inc(x_15); +lean_dec(x_14); +x_16 = lean_apply_10(x_15, lean_box(0), x_13, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); +return x_16; +} +else +{ +lean_object* x_17; lean_object* x_18; +x_17 = lean_ctor_get(x_4, 0); +lean_inc(x_17); +lean_dec(x_4); +x_18 = l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1(x_1, x_2, x_17, x_3, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); +return x_18; } } -lean_object* l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1(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) { +} +lean_object* l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1(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, lean_object* x_12) { _start: { if (lean_obj_tag(x_2) == 0) { -lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; -lean_dec(x_3); -x_12 = lean_ctor_get(x_1, 0); -lean_inc(x_12); -lean_dec(x_1); -x_13 = lean_ctor_get(x_12, 1); +lean_object* x_13; lean_object* x_14; lean_object* x_15; +lean_dec(x_4); +x_13 = lean_ctor_get(x_1, 0); lean_inc(x_13); -lean_dec(x_12); -x_14 = lean_box(0); -x_15 = lean_apply_10(x_13, lean_box(0), x_14, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11); +lean_dec(x_1); +x_14 = lean_ctor_get(x_13, 1); +lean_inc(x_14); +lean_dec(x_13); +x_15 = lean_apply_10(x_14, lean_box(0), x_3, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); return x_15; } else { lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; +lean_dec(x_3); x_16 = lean_ctor_get(x_2, 0); lean_inc(x_16); x_17 = lean_ctor_get(x_2, 1); @@ -25333,17 +25450,17 @@ lean_inc(x_17); lean_dec(x_2); x_18 = lean_ctor_get(x_1, 1); lean_inc(x_18); -lean_inc(x_3); +lean_inc(x_4); lean_inc(x_1); -x_19 = lean_alloc_closure((void*)(l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1), 11, 3); +x_19 = lean_alloc_closure((void*)(l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1), 11, 3); lean_closure_set(x_19, 0, x_16); lean_closure_set(x_19, 1, x_1); -lean_closure_set(x_19, 2, x_3); -x_20 = lean_alloc_closure((void*)(l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__2___boxed), 12, 3); +lean_closure_set(x_19, 2, x_4); +x_20 = lean_alloc_closure((void*)(l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__2), 12, 3); lean_closure_set(x_20, 0, x_1); lean_closure_set(x_20, 1, x_17); -lean_closure_set(x_20, 2, x_3); -x_21 = lean_apply_12(x_18, lean_box(0), lean_box(0), x_19, x_20, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11); +lean_closure_set(x_20, 2, x_4); +x_21 = lean_apply_12(x_18, lean_box(0), lean_box(0), x_19, x_20, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); return x_21; } } @@ -25376,37 +25493,129 @@ x_15 = l_Lean_Elab_Term_StructInst_Struct_fields(x_1); x_16 = !lean_is_exclusive(x_2); if (x_16 == 0) { -lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; +lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; x_17 = lean_ctor_get(x_2, 0); x_18 = lean_array_push(x_17, x_1); lean_ctor_set(x_2, 0, x_18); x_19 = l_Lean_Elab_Term_StructInst_DefaultFields_step___closed__1; -x_20 = l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1(x_19, x_15, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_14); -return x_20; +x_20 = lean_box(0); +x_21 = l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1(x_19, x_15, x_20, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_14); +if (lean_obj_tag(x_21) == 0) +{ +uint8_t x_22; +x_22 = !lean_is_exclusive(x_21); +if (x_22 == 0) +{ +return x_21; } else { -lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; -x_21 = lean_ctor_get(x_2, 0); -x_22 = lean_ctor_get(x_2, 1); -x_23 = lean_ctor_get(x_2, 2); +lean_object* x_23; lean_object* x_24; lean_object* x_25; +x_23 = lean_ctor_get(x_21, 0); +x_24 = lean_ctor_get(x_21, 1); +lean_inc(x_24); lean_inc(x_23); -lean_inc(x_22); -lean_inc(x_21); -lean_dec(x_2); -x_24 = lean_array_push(x_21, x_1); -x_25 = lean_alloc_ctor(0, 3, 0); -lean_ctor_set(x_25, 0, x_24); -lean_ctor_set(x_25, 1, x_22); -lean_ctor_set(x_25, 2, x_23); -x_26 = l_Lean_Elab_Term_StructInst_DefaultFields_step___closed__1; -x_27 = l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1(x_26, x_15, x_25, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_14); -return x_27; +lean_dec(x_21); +x_25 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_25, 0, x_23); +lean_ctor_set(x_25, 1, x_24); +return x_25; } } else { -uint8_t x_28; +uint8_t x_26; +x_26 = !lean_is_exclusive(x_21); +if (x_26 == 0) +{ +return x_21; +} +else +{ +lean_object* x_27; lean_object* x_28; lean_object* x_29; +x_27 = lean_ctor_get(x_21, 0); +x_28 = lean_ctor_get(x_21, 1); +lean_inc(x_28); +lean_inc(x_27); +lean_dec(x_21); +x_29 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_29, 0, x_27); +lean_ctor_set(x_29, 1, x_28); +return x_29; +} +} +} +else +{ +lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; +x_30 = lean_ctor_get(x_2, 0); +x_31 = lean_ctor_get(x_2, 1); +x_32 = lean_ctor_get(x_2, 2); +lean_inc(x_32); +lean_inc(x_31); +lean_inc(x_30); +lean_dec(x_2); +x_33 = lean_array_push(x_30, x_1); +x_34 = lean_alloc_ctor(0, 3, 0); +lean_ctor_set(x_34, 0, x_33); +lean_ctor_set(x_34, 1, x_31); +lean_ctor_set(x_34, 2, x_32); +x_35 = l_Lean_Elab_Term_StructInst_DefaultFields_step___closed__1; +x_36 = lean_box(0); +x_37 = l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1(x_35, x_15, x_36, x_34, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_14); +if (lean_obj_tag(x_37) == 0) +{ +lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; +x_38 = lean_ctor_get(x_37, 0); +lean_inc(x_38); +x_39 = lean_ctor_get(x_37, 1); +lean_inc(x_39); +if (lean_is_exclusive(x_37)) { + lean_ctor_release(x_37, 0); + lean_ctor_release(x_37, 1); + x_40 = x_37; +} else { + lean_dec_ref(x_37); + x_40 = lean_box(0); +} +if (lean_is_scalar(x_40)) { + x_41 = lean_alloc_ctor(0, 2, 0); +} else { + x_41 = x_40; +} +lean_ctor_set(x_41, 0, x_38); +lean_ctor_set(x_41, 1, x_39); +return x_41; +} +else +{ +lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; +x_42 = lean_ctor_get(x_37, 0); +lean_inc(x_42); +x_43 = lean_ctor_get(x_37, 1); +lean_inc(x_43); +if (lean_is_exclusive(x_37)) { + lean_ctor_release(x_37, 0); + lean_ctor_release(x_37, 1); + x_44 = x_37; +} else { + lean_dec_ref(x_37); + x_44 = lean_box(0); +} +if (lean_is_scalar(x_44)) { + x_45 = lean_alloc_ctor(1, 2, 0); +} else { + x_45 = x_44; +} +lean_ctor_set(x_45, 0, x_42); +lean_ctor_set(x_45, 1, x_43); +return x_45; +} +} +} +else +{ +uint8_t x_46; lean_dec(x_9); lean_dec(x_8); lean_dec(x_7); @@ -25416,40 +25625,31 @@ lean_dec(x_4); lean_dec(x_3); lean_dec(x_2); lean_dec(x_1); -x_28 = !lean_is_exclusive(x_11); -if (x_28 == 0) +x_46 = !lean_is_exclusive(x_11); +if (x_46 == 0) { -lean_object* x_29; lean_object* x_30; -x_29 = lean_ctor_get(x_11, 0); -lean_dec(x_29); -x_30 = lean_box(0); -lean_ctor_set(x_11, 0, x_30); +lean_object* x_47; lean_object* x_48; +x_47 = lean_ctor_get(x_11, 0); +lean_dec(x_47); +x_48 = lean_box(0); +lean_ctor_set(x_11, 0, x_48); return x_11; } else { -lean_object* x_31; lean_object* x_32; lean_object* x_33; -x_31 = lean_ctor_get(x_11, 1); -lean_inc(x_31); +lean_object* x_49; lean_object* x_50; lean_object* x_51; +x_49 = lean_ctor_get(x_11, 1); +lean_inc(x_49); lean_dec(x_11); -x_32 = lean_box(0); -x_33 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_33, 0, x_32); -lean_ctor_set(x_33, 1, x_31); -return x_33; +x_50 = lean_box(0); +x_51 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_51, 0, x_50); +lean_ctor_set(x_51, 1, x_49); +return x_51; } } } } -lean_object* l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__2___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, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12) { -_start: -{ -lean_object* x_13; -x_13 = l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12); -lean_dec(x_4); -return x_13; -} -} lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_propagateLoop_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -27092,7 +27292,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } -lean_object* l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_6252_(lean_object* x_1) { +lean_object* l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_6337_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -27396,10 +27596,10 @@ l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__ lean_mark_persistent(l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__2); l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__3 = _init_l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__3(); lean_mark_persistent(l_Lean_Elab_Term_StructInst_DefaultFields_tryToSynthesizeDefault_loop___closed__3); -l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1 = _init_l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1(); -lean_mark_persistent(l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1); -l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__2 = _init_l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__2(); -lean_mark_persistent(l_List_forM___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__2); +l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1 = _init_l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1(); +lean_mark_persistent(l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__1); +l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__2 = _init_l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__2(); +lean_mark_persistent(l_List_forIn_loop___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__1___lambda__1___closed__2); l_Lean_Elab_Term_StructInst_DefaultFields_step___closed__1 = _init_l_Lean_Elab_Term_StructInst_DefaultFields_step___closed__1(); lean_mark_persistent(l_Lean_Elab_Term_StructInst_DefaultFields_step___closed__1); l_Lean_Elab_Term_StructInst_DefaultFields_propagateLoop___closed__1 = _init_l_Lean_Elab_Term_StructInst_DefaultFields_propagateLoop___closed__1(); @@ -27425,7 +27625,7 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_StructInst_elabStructInst___c res = l___regBuiltin_Lean_Elab_Term_StructInst_elabStructInst(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -res = l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_6252_(lean_io_mk_world()); +res = l_Lean_Elab_Term_StructInst_initFn____x40_Lean_Elab_StructInst___hyg_6337_(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)); diff --git a/stage0/stdlib/Lean/Elab/Tactic/Basic.c b/stage0/stdlib/Lean/Elab/Tactic/Basic.c index 9e3849b55b..29da6cdf23 100644 --- a/stage0/stdlib/Lean/Elab/Tactic/Basic.c +++ b/stage0/stdlib/Lean/Elab/Tactic/Basic.c @@ -474,12 +474,11 @@ lean_object* l_Lean_Elab_Tactic_adaptExpander(lean_object*, lean_object*, lean_o lean_object* l_Lean_Elab_Tactic_evalCase_match__1(lean_object*); lean_object* l_Lean_Elab_Tactic_evalTraceState___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_focusAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3754____closed__1; lean_object* l_Lean_Elab_Tactic_getFVarIds(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_evalTactic___lambda__1___closed__2; lean_object* l_Lean_Meta_getMVars___at_Lean_Elab_Tactic_ensureHasNoMVars___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_AssocList_find_x3f___at_Lean_Elab_Tactic_evalTactic___spec__6(lean_object*, lean_object*); -lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3754_(lean_object*); +lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3755_(lean_object*); lean_object* l_Array_toList___rarg(lean_object*); lean_object* l_Lean_Elab_Tactic_ensureHasType(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_Elab_Tactic_withMacroExpansion___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -577,6 +576,7 @@ lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__1; lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_evalClear___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1; extern lean_object* l_Array_forInUnsafe_loop___at_Lean_mkSepArray___spec__1___closed__1; +lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3755____closed__1; lean_object* l_Lean_Elab_Term_reportUnsolvedGoals___closed__2; extern lean_object* l_Lean_Elab_Term_expandFunBinders_loop___closed__4; extern lean_object* l_Lean_Elab_Term_expandFunBinders_loop___closed__17; @@ -14672,7 +14672,7 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } -static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3754____closed__1() { +static lean_object* _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3755____closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -14682,11 +14682,11 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3754_(lean_object* x_1) { +lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3755_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; -x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3754____closed__1; +x_2 = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3755____closed__1; x_3 = l_Lean_registerTraceClass(x_2, x_1); return x_3; } @@ -15162,9 +15162,9 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalOrelse___closed__1); res = l___regBuiltin_Lean_Elab_Tactic_evalOrelse(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3754____closed__1 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3754____closed__1(); -lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3754____closed__1); -res = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3754_(lean_io_mk_world()); +l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3755____closed__1 = _init_l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3755____closed__1(); +lean_mark_persistent(l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3755____closed__1); +res = l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Basic___hyg_3755_(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)); diff --git a/stage0/stdlib/Lean/Elab/Tactic/Binders.c b/stage0/stdlib/Lean/Elab/Tactic/Binders.c index 21c40bf942..33a590bba7 100644 --- a/stage0/stdlib/Lean/Elab/Tactic/Binders.c +++ b/stage0/stdlib/Lean/Elab/Tactic/Binders.c @@ -46,6 +46,7 @@ lean_object* l___regBuiltin_Lean_Elab_Tactic_expandLetBangTactic___closed__1; extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_299____closed__5; lean_object* l_Lean_Elab_Tactic_expandLetBangTactic(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Tactic_Binders_0__Lean_Elab_Tactic_liftTermBinderSyntax___closed__3; +extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__1; lean_object* l_Lean_Elab_Tactic_expandLetRecTactic(lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Elab_Tactic_expandLetTactic___closed__1; extern lean_object* l_myMacro____x40_Init_Data_ToString_Macro___hyg_39____closed__15; @@ -53,7 +54,6 @@ lean_object* l_Lean_Elab_Tactic_expandShowTactic___closed__7; lean_object* lean_name_mk_string(lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Elab_Tactic_expandLetTactic___closed__2; lean_object* l_Lean_Elab_Tactic_expandShowTactic___closed__10; -extern lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__1; extern lean_object* l_Lean_mkAppStx___closed__6; lean_object* l___private_Lean_Elab_Tactic_Binders_0__Lean_Elab_Tactic_liftTermBinderSyntax___closed__5; lean_object* l___regBuiltin_Lean_Elab_Tactic_expandHaveTactic___closed__1; @@ -557,7 +557,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_myMacro____x40_Init_Tactics___hyg_31____closed__2; -x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__1; +x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } diff --git a/stage0/stdlib/Lean/Elab/Term.c b/stage0/stdlib/Lean/Elab/Term.c index d8963e2191..d73985b19e 100644 --- a/stage0/stdlib/Lean/Elab/Term.c +++ b/stage0/stdlib/Lean/Elab/Term.c @@ -256,6 +256,7 @@ lean_object* l_Lean_Elab_Term_Lean_Elab_Term___instance__8___closed__2; lean_object* l_Lean_Elab_Term_Lean_Elab_Term___instance__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_List_repr___rarg___closed__3; lean_object* l___regBuiltin_Lean_Elab_Term_elabTypeStx___closed__2; +lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7470____closed__1; lean_object* l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__7; lean_object* l_Lean_Elab_Term_Lean_Elab_Term___instance__8___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -294,7 +295,6 @@ lean_object* l_Lean_Elab_Term_Lean_Elab_Term___instance__12___closed__7; lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_useImplicitLambda_x3f_match__1(lean_object*); lean_object* l_Lean_Elab_Term_Lean_Elab_Term___instance__8___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_mkExplicitBinder___closed__8; -lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7468____closed__1; lean_object* l_Lean_Elab_Term_Lean_Elab_Term___instance__1___closed__1; extern lean_object* l_Lean_mkAppStx___closed__8; lean_object* l_Lean_Elab_Term_elabNumLit_match__1___rarg(lean_object*, lean_object*, lean_object*); @@ -443,6 +443,7 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_useImplicitLambda_x3f_ lean_object* l_Lean_Elab_Term_mkConst___closed__2; lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe_match__4(lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns_match__1(lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__1; lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_mkAppOptM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_tryPureCoe_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -476,7 +477,6 @@ lean_object* l_Lean_Expr_fvarId_x21(lean_object*); lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___closed__7; lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__2(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_TermElabM_run_x27___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__2; lean_object* l_Lean_Elab_Term_Lean_Elab_Term___instance__11___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_applyResult_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabCharLit_match__1___rarg(lean_object*, lean_object*, lean_object*); @@ -528,10 +528,11 @@ lean_object* l_Lean_Elab_Term_mkTypeMismatchError_match__1___rarg(lean_object*, lean_object* l___regBuiltin_Lean_Elab_Term_elabCharLit(lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabOptLevel___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFnsAux_match__2___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712_(lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714_(lean_object*); lean_object* l_Lean_Elab_Term_setElabConfig(lean_object*); lean_object* l_Lean_Elab_Term_getLetRecsToLift(lean_object*); lean_object* l_Lean_Elab_Term_liftLevelM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__2; lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_813_(lean_object*); extern lean_object* l_Lean_MessageData_nil___closed__1; lean_object* l_Lean_Syntax_getId(lean_object*); @@ -572,7 +573,6 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_Lean_Elab_Term___inst lean_object* l_Lean_Elab_Term_expandArrayLit___closed__11; lean_object* l_Lean_Elab_Term_getMainModule(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Meta_throwTypeExcepted___rarg___closed__2; -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__1; lean_object* l_Lean_Elab_Term_mkTermElabAttribute(lean_object*); extern lean_object* l_Lean_numLitKind___closed__2; lean_object* l_Std_AssocList_find_x3f___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabUsingElabFns___spec__6___boxed(lean_object*, lean_object*); @@ -986,7 +986,7 @@ lean_object* l_Lean_Elab_Term_logUnassignedUsingErrorInfos_match__2___rarg(lean_ lean_object* l_Lean_Elab_Term_throwErrorIfErrors(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*); extern lean_object* l_Lean_Meta_isLevelDefEq___rarg___lambda__2___closed__4; -lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7468_(lean_object*); +lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7470_(lean_object*); lean_object* l_Lean_Elab_Term_elabByTactic_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_MVarErrorInfo_logError___spec__3(lean_object*, size_t, size_t, lean_object*); extern lean_object* l_Lean_Expr_Lean_Expr___instance__11___closed__1; @@ -29681,7 +29681,7 @@ lean_dec(x_3); return x_9; } } -static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__1() { +static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__1() { _start: { lean_object* x_1; @@ -29689,21 +29689,21 @@ x_1 = lean_mk_string("letrec"); return x_1; } } -static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__2() { +static lean_object* _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Util___hyg_834____closed__1; -x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__1; +x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712_(lean_object* x_1) { +lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; -x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__2; +x_2 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__2; x_3 = l_Lean_registerTraceClass(x_2, x_1); return x_3; } @@ -29870,7 +29870,7 @@ lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; lean x_89 = lean_ctor_get(x_83, 1); lean_inc(x_89); lean_dec(x_83); -x_90 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__2; +x_90 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__2; x_91 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(x_90, x_2, x_3, x_4, x_5, x_6, x_7, x_89); x_92 = lean_ctor_get(x_91, 0); lean_inc(x_92); @@ -29912,7 +29912,7 @@ lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean x_49 = lean_ctor_get(x_43, 1); lean_inc(x_49); lean_dec(x_43); -x_50 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__2; +x_50 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__2; x_51 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(x_50, x_2, x_3, x_4, x_5, x_6, x_7, x_49); x_52 = lean_ctor_get(x_51, 0); lean_inc(x_52); @@ -29989,7 +29989,7 @@ x_37 = l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__ x_38 = lean_alloc_ctor(10, 2, 0); lean_ctor_set(x_38, 0, x_36); lean_ctor_set(x_38, 1, x_37); -x_39 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__2; +x_39 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__2; x_40 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_39, x_38, x_2, x_3, x_4, x_5, x_6, x_7, x_32); x_41 = lean_ctor_get(x_40, 1); lean_inc(x_41); @@ -30047,7 +30047,7 @@ x_73 = l_Array_foldlMUnsafe_fold___at_Lean_withNestedTraces___spec__5___closed__ x_74 = lean_alloc_ctor(10, 2, 0); lean_ctor_set(x_74, 0, x_72); lean_ctor_set(x_74, 1, x_73); -x_75 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__2; +x_75 = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__2; x_76 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_75, x_74, x_2, x_3, x_4, x_5, x_6, x_7, x_57); x_77 = lean_ctor_get(x_76, 1); lean_inc(x_77); @@ -37269,7 +37269,7 @@ x_8 = l_Lean_Elab_Term_Lean_Elab_Term___instance__13___rarg(x_1, x_2, x_3, x_4, return x_8; } } -static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7468____closed__1() { +static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7470____closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -37279,7 +37279,7 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7468_(lean_object* x_1) { +lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7470_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; @@ -37291,7 +37291,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; x_4 = lean_ctor_get(x_3, 1); lean_inc(x_4); lean_dec(x_3); -x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7468____closed__1; +x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7470____closed__1; x_6 = l_Lean_registerTraceClass(x_5, x_4); if (lean_obj_tag(x_6) == 0) { @@ -37740,11 +37740,11 @@ l_Lean_Elab_Term_mkAuxName___closed__2 = _init_l_Lean_Elab_Term_mkAuxName___clos lean_mark_persistent(l_Lean_Elab_Term_mkAuxName___closed__2); l_Lean_Elab_Term_mkAuxName___closed__3 = _init_l_Lean_Elab_Term_mkAuxName___closed__3(); lean_mark_persistent(l_Lean_Elab_Term_mkAuxName___closed__3); -l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__1(); -lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__1); -l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__2(); -lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712____closed__2); -res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5712_(lean_io_mk_world()); +l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__1 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__1(); +lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__1); +l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__2 = _init_l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__2(); +lean_mark_persistent(l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714____closed__2); +res = l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_5714_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); l_Lean_Elab_Term_isLetRecAuxMVar___closed__1 = _init_l_Lean_Elab_Term_isLetRecAuxMVar___closed__1(); @@ -37959,9 +37959,9 @@ l_Lean_Elab_Term_Lean_Elab_Term___instance__13___rarg___closed__2 = _init_l_Lean lean_mark_persistent(l_Lean_Elab_Term_Lean_Elab_Term___instance__13___rarg___closed__2); l_Lean_Elab_Term_Lean_Elab_Term___instance__13___rarg___closed__3 = _init_l_Lean_Elab_Term_Lean_Elab_Term___instance__13___rarg___closed__3(); lean_mark_persistent(l_Lean_Elab_Term_Lean_Elab_Term___instance__13___rarg___closed__3); -l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7468____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7468____closed__1(); -lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7468____closed__1); -res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7468_(lean_io_mk_world()); +l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7470____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7470____closed__1(); +lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7470____closed__1); +res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_7470_(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)); diff --git a/stage0/stdlib/Lean/Meta/RecursorInfo.c b/stage0/stdlib/Lean/Meta/RecursorInfo.c index 5be40d6149..bbbafd9100 100644 --- a/stage0/stdlib/Lean/Meta/RecursorInfo.c +++ b/stage0/stdlib/Lean/Meta/RecursorInfo.c @@ -17,9 +17,9 @@ lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim_ lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getParamsPos___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Array_qsort_sort___at_Lean_registerParametricAttribute___spec__2___rarg___closed__1; lean_object* l_Lean_Meta_recursorAttribute; +lean_object* l_Array_qsort_sort___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__5___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__3___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getNumParams___boxed(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3___closed__1; lean_object* l_Lean_Meta_brecOnSuffix___closed__1; lean_object* l_Lean_Meta_binductionOnSuffix; lean_object* lean_array_set(lean_object*, lean_object*, lean_object*); @@ -36,10 +36,10 @@ lean_object* lean_nat_div(lean_object*, lean_object*); lean_object* l_Lean_PersistentEnvExtension_getModuleEntries___rarg(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getIndicesPos_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosIfAuxRecursor_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_registerParametricAttribute___rarg___lambda__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_isExprDefEq___at_Lean_Meta_isExprDefEqGuarded___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Init_Core___instance__33; uint8_t l_USize_decEq(size_t, size_t); lean_object* l_List_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getUnivLevelPos___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -50,22 +50,24 @@ lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_syntaxToMajorPos_ma lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_checkMotiveResultType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__4; extern lean_object* l_Lean_getConstInfoInduct___rarg___lambda__1___closed__2; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux_match__2(lean_object*); lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__2___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Init_LeanInit___instance__9; uint8_t l_Lean_Name_quickLt(lean_object*, lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__4; lean_object* l_Lean_Meta_RecursorInfo_isMinor___boxed(lean_object*, lean_object*); lean_object* l_Lean_Meta_inferType___at___private_Lean_Meta_InferType_0__Lean_Meta_inferAppType___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__3___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_mkRecursorInfo_match__2(lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_registerInternalExceptionId___closed__2; lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__1(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_mkBRecOnName(lean_object*); +lean_object* l_Lean_ofExcept___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Array_empty___closed__1; extern lean_object* l_Init_Data_Repr___instance__2___closed__2; lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__3___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -77,15 +79,15 @@ lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_checkMotiveResultTy uint8_t lean_name_eq(lean_object*, lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___lambda__1___closed__1; uint8_t l_Lean_Meta_RecursorInfo_isMinor(lean_object*, lean_object*); -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__8; lean_object* l_Lean_Meta_recOnSuffix; +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__8; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_checkMotive___closed__1; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_checkMotiveResultType___closed__1; lean_object* l_Lean_Meta_RecursorInfo_numParams(lean_object*); -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__7; lean_object* lean_array_push(lean_object*, lean_object*); lean_object* lean_array_get_size(lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__7; lean_object* lean_string_append(lean_object*, lean_object*); lean_object* l_Lean_fmt___at_Lean_Position_Lean_Data_Position___instance__2___spec__1(lean_object*); lean_object* l_Array_binSearchAux___at_Lean_Meta_getMajorPos_x3f___spec__2(lean_object*, lean_object*, lean_object*, lean_object*); @@ -93,11 +95,10 @@ lean_object* l_List_range(lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_checkMotive___closed__4; extern lean_object* l_Lean_Expr_getAppArgs___closed__1; lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getParamsPos___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3___lambda__1___boxed(lean_object*); lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_995____spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__3; lean_object* l_Lean_getConstInfoInduct___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoForKernelRec___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_List_repr___rarg___closed__3; -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__3; lean_object* l_List_toStringAux___at_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___spec__6___boxed(lean_object*, lean_object*); extern lean_object* l_Init_Data_Repr___instance__9___rarg___closed__2; lean_object* l_Lean_Meta_mkRecursorInfo_match__1___rarg(lean_object*, lean_object*, lean_object*); @@ -105,11 +106,13 @@ uint8_t l_USize_decLt(size_t, size_t); lean_object* l_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___closed__15; extern lean_object* l_Lean_auxRecExt; lean_object* l_Lean_Expr_occurs___lambda__1___boxed(lean_object*, lean_object*); +lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3___closed__1; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMotiveLevel___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_nat_add(lean_object*, lean_object*); lean_object* l_Lean_Meta_mkCasesOnName(lean_object*); -lean_object* l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*); +lean_object* l_Array_qsort_sort___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__5(lean_object*, lean_object*, lean_object*); +lean_object* l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_toStringAux___at_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___spec__4___boxed(lean_object*, lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive_match__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -123,11 +126,10 @@ lean_object* l_List_replicate___rarg(lean_object*, lean_object*); lean_object* l_Lean_Meta_casesOnSuffix; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___closed__6; lean_object* l_Lean_Meta_RecursorInfo_numParams___boxed(lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__5; lean_object* l_List_toStringAux___at_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___spec__4___closed__1; lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___closed__10; -lean_object* l_Array_qsort_sort___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__5(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__5; lean_object* l_Lean_throwError___at_Lean_Meta_getMVarDecl___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_getConstInfoRec___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosIfAuxRecursor_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_RecursorVal_getMajorIdx(lean_object*); @@ -151,19 +153,19 @@ lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_checkMotive(lean_ob lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive_match__3(lean_object*); lean_object* l_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___closed__16; lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__2(lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux_match__2___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069_(lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070_(lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_checkMotive___closed__2; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getIndicesPos(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__2(lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___closed__2; extern lean_object* l_Init_Data_Repr___instance__9___rarg___closed__1; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___closed__8; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_syntaxToMajorPos_match__2(lean_object*); uint8_t l_Array_contains___at_Lean_Meta_CheckAssignment_check___spec__2(lean_object*, lean_object*); +lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_toStringAux___at_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___spec__2(uint8_t, lean_object*); lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getIndicesPos___spec__1(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__3___boxed(lean_object*, lean_object*, lean_object*); lean_object* lean_array_get(lean_object*, lean_object*, lean_object*); lean_object* l_List_toString___at_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___spec__1(lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_syntaxToMajorPos___closed__3; @@ -173,7 +175,7 @@ lean_object* l_Lean_Meta_Lean_Meta_RecursorInfo___instance__1_match__1(lean_obje lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_syntaxToMajorPos___closed__4; lean_object* l_Lean_getConstInfoRec___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosIfAuxRecursor_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux___spec__1___boxed(lean_object**); -lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux___spec__1___closed__1; lean_object* l_Lean_ConstantInfo_name(lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getUnivLevelPos_match__1___rarg(lean_object*, lean_object*, lean_object*); @@ -186,18 +188,15 @@ lean_object* l_List_map___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRec lean_object* l_List_toStringAux___at_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___spec__8___closed__2; uint8_t l_Lean_LocalDecl_binderInfo(lean_object*); lean_object* lean_st_mk_ref(lean_object*, lean_object*); -lean_object* l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getUnivLevelPos___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux___spec__1___closed__2; lean_object* l_Lean_Meta_RecursorInfo_numMinors___boxed(lean_object*); -lean_object* l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6___closed__1; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getNumParams(lean_object*, lean_object*, lean_object*); lean_object* lean_name_mk_string(lean_object*, lean_object*); -lean_object* l_Array_qsort_sort___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__5___boxed(lean_object*, lean_object*, lean_object*); extern lean_object* l_List_repr___rarg___closed__2; lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___lambda__2(lean_object*, lean_object*, lean_object*); -lean_object* l_Std_RBNode_fold___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__4(lean_object*, lean_object*); lean_object* l_List_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getUnivLevelPos___spec__1___closed__2; +lean_object* l_Std_RBNode_fold___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__4(lean_object*, lean_object*); lean_object* l_Lean_Meta_RecursorInfo_motivePos___boxed(lean_object*); lean_object* l_Lean_getConstInfo___at_Lean_Meta_getParamNamesImp___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -207,10 +206,10 @@ lean_object* l_addParenHeuristic(lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___lambda__1___closed__2; lean_object* l_List_toString___at_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___spec__7(lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive_match__2___rarg(lean_object*, lean_object*); +lean_object* l_Lean_ofExcept___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___closed__13; extern lean_object* l_Lean_persistentEnvExtensionsRef; lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getParamsPos___spec__2___closed__2; -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_registerParametricAttribute___rarg___closed__1; lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getParamsPos___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_registerParametricAttribute___rarg___closed__2; @@ -234,14 +233,13 @@ extern lean_object* l_Lean_ParametricAttribute_Lean_Attributes___instance__6___c uint8_t l_Lean_BinderInfo_isInstImplicit(uint8_t); lean_object* l_List_toStringAux___at_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___spec__2___boxed(lean_object*, lean_object*); lean_object* l_List_toString___at_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___spec__5(lean_object*); -lean_object* l_Lean_ofExcept___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_getMajorPos_x3f___boxed(lean_object*, lean_object*); lean_object* l_Lean_Meta_RecursorInfo_numIndices(lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux_match__3(lean_object*); size_t lean_usize_of_nat(lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_ConstantInfo_type(lean_object*); -lean_object* l_Lean_ofExcept___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_syntaxToMajorPos___closed__2; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMotiveLevel_match__1(lean_object*); lean_object* l_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2(lean_object*); @@ -250,14 +248,12 @@ lean_object* l_Lean_Meta_mkRecursorInfo(lean_object*, lean_object*, lean_object* lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getParamsPos(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_RecursorVal_getInduct(lean_object*); -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_ConstantInfo_lparams(lean_object*); lean_object* l_Lean_Meta_casesOnSuffix___closed__1; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim_match__2___rarg(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Expr_FindImpl_initCache; lean_object* l_Array_back___at___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processAssignmentFOApproxAux___spec__1(lean_object*); extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1; -lean_object* l_Std_RBNode_fold___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__4___boxed(lean_object*, lean_object*); lean_object* l_List_redLength___rarg(lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___closed__1; lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*); @@ -276,15 +272,17 @@ lean_object* l_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___clo lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosIfAuxRecursor_x3f_match__1(lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMotiveLevel_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_RecursorInfo_firstIndexPos___boxed(lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__3(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___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux_match__1(lean_object*); extern lean_object* l_Lean_registerParametricAttribute___rarg___closed__3; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getIndicesPos___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__3(lean_object*, lean_object*, lean_object*); lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getIndicesPos___spec__2___closed__1; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_syntaxToMajorPos___boxed(lean_object*); -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__3(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_mkRecursorInfo_match__1(lean_object*); extern lean_object* l_List_reprAux___rarg___closed__1; +lean_object* l_Std_RBNode_fold___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__4___boxed(lean_object*, lean_object*); lean_object* l_List_toStringAux___at_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___spec__8(uint8_t, lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_addMessageContextPartial___at_Lean_Core_Lean_CoreM___instance__6___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); @@ -292,10 +290,10 @@ lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoCore_ lean_object* l_Lean_Meta_mkBInductionOnName(lean_object*); lean_object* l_Lean_Meta_Lean_Meta_RecursorInfo___instance__1_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMotiveLevel___closed__2; -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___closed__3; lean_object* l_Lean_Meta_RecursorInfo_motivePos(lean_object*); uint8_t l_Lean_Expr_isFVar(lean_object*); +lean_object* l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_syntaxToMajorPos_match__1(lean_object*); lean_object* l_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___closed__14; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMotiveLevel(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -311,12 +309,12 @@ lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_RecursorInfo_0__L lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getUnivLevelPos(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Init_Data_Repr___instance__2___closed__1; lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux___spec__1___lambda__1___boxed(lean_object**); -lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3(lean_object*, lean_object*); lean_object* l_List_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getUnivLevelPos___spec__1___lambda__1___boxed(lean_object*, lean_object*); lean_object* l_Array_toList___rarg(lean_object*); -lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3___lambda__1___boxed(lean_object*); uint8_t l_Lean_TagDeclarationExtension_isTagged(lean_object*, lean_object*, lean_object*); lean_object* l_Array_getIdx_x3f___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___spec__1___boxed(lean_object*, lean_object*); +lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3(lean_object*, lean_object*); lean_object* lean_mk_array(lean_object*, lean_object*); lean_object* l_List_map___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoForKernelRec___spec__3(lean_object*); lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getParamsPos___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -325,12 +323,13 @@ lean_object* l_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___clo lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_object*); lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getParamsPos___spec__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* l_Std_Range_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getIndicesPos___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3___lambda__1(lean_object*); lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux___spec__2___closed__2; lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_mkRecOnName(lean_object*); +lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_getConstInfoRec___rarg___lambda__1___closed__2; lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__3___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___closed__1; lean_object* l_Lean_Expr_FindImpl_findM_x3f_visit(lean_object*, size_t, lean_object*, lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoForKernelRec___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -339,35 +338,36 @@ lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getUnivLevelPos___b lean_object* l_Array_getIdx_x3f___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___spec__1(lean_object*, lean_object*); lean_object* l_Lean_Meta_mkRecursorInfo_match__2___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___closed__4; +lean_object* l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6___closed__1; lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux___spec__2___closed__1; -lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Meta_Lean_Meta_Basic___instance__11___rarg___closed__2; +uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__8(lean_object*, lean_object*, size_t, size_t); lean_object* l_Array_findIdx_x3f_loop___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_ParametricAttribute_getParam___at_Lean_Meta_getMajorPos_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*); extern lean_object* l_System_FilePath_dirName___closed__1; lean_object* l_Lean_Meta_binductionOnSuffix___closed__1; lean_object* l_List_lengthAux___rarg(lean_object*, lean_object*); lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoAux_match__3___rarg(lean_object*, lean_object*); -lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__7(lean_object*, lean_object*); +lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__7(lean_object*, lean_object*); lean_object* l_Lean_mkLevelParam(lean_object*); lean_object* l_List_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getUnivLevelPos___spec__1___closed__1; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim_match__2(lean_object*); lean_object* l_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___closed__9; uint8_t lean_level_eq(lean_object*, lean_object*); lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__3___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__6; -uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__8(lean_object*, lean_object*, size_t, size_t); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__6; +lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3___lambda__1(lean_object*); extern lean_object* l_Lean_Meta_Lean_Meta_Basic___instance__11___rarg___closed__1; lean_object* l_Lean_registerParametricAttribute___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkConst(lean_object*, lean_object*); lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive___spec__3___lambda__2(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__1; lean_object* l_List_map___at___private_Lean_Meta_RecursorInfo_0__Lean_Meta_mkRecursorInfoForKernelRec___spec__4(lean_object*, lean_object*); -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__1; lean_object* l_Lean_Meta_recOnSuffix___closed__1; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getMajorPosDepElim___closed__3; lean_object* l_List_toStringAux___at_Lean_Meta_RecursorInfo_Lean_Meta_RecursorInfo___instance__2___spec__4(uint8_t, lean_object*); extern lean_object* l_Array_findIdxM_x3f___rarg___closed__1; -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__2; +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__2; lean_object* l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_getProduceMotiveAndRecursive_match__1(lean_object*); uint8_t l_Lean_Expr_isSort(lean_object*); lean_object* l_Lean_Meta_Lean_Meta_RecursorInfo___instance__1___closed__1; @@ -9303,7 +9303,7 @@ return x_18; } } } -lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__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_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__2___rarg(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; uint8_t x_8; @@ -9341,15 +9341,15 @@ return x_14; } } } -lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__2(lean_object* x_1) { +lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__2(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__2___rarg___boxed), 5, 0); +x_2 = lean_alloc_closure((void*)(l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__2___rarg___boxed), 5, 0); return x_2; } } -lean_object* l_Lean_ofExcept___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +lean_object* l_Lean_ofExcept___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__1(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) @@ -9361,7 +9361,7 @@ x_7 = lean_alloc_ctor(2, 1, 0); lean_ctor_set(x_7, 0, x_6); x_8 = lean_alloc_ctor(0, 1, 0); lean_ctor_set(x_8, 0, x_7); -x_9 = l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__2___rarg(x_8, x_2, x_3, x_4, x_5); +x_9 = l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__2___rarg(x_8, x_2, x_3, x_4, x_5); return x_9; } else @@ -9376,7 +9376,7 @@ return x_11; } } } -lean_object* l_Std_RBNode_fold___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__4(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_RBNode_fold___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__4(lean_object* x_1, lean_object* x_2) { _start: { if (lean_obj_tag(x_2) == 0) @@ -9390,7 +9390,7 @@ x_3 = lean_ctor_get(x_2, 0); x_4 = lean_ctor_get(x_2, 1); x_5 = lean_ctor_get(x_2, 2); x_6 = lean_ctor_get(x_2, 3); -x_7 = l_Std_RBNode_fold___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__4(x_1, x_3); +x_7 = l_Std_RBNode_fold___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__4(x_1, x_3); lean_inc(x_5); lean_inc(x_4); x_8 = lean_alloc_ctor(0, 2, 0); @@ -9403,7 +9403,7 @@ goto _start; } } } -static lean_object* _init_l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6___closed__1() { +static lean_object* _init_l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -9415,7 +9415,7 @@ lean_ctor_set(x_3, 1, x_2); return x_3; } } -lean_object* l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6(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* l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6(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: { uint8_t x_7; @@ -9435,7 +9435,7 @@ return x_9; else { lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; -x_10 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6___closed__1; +x_10 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6___closed__1; x_11 = lean_array_get(x_10, x_4, x_6); lean_inc(x_1); lean_inc(x_3); @@ -9468,7 +9468,7 @@ goto _start; } } } -lean_object* l_Array_qsort_sort___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__5(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Array_qsort_sort___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__5(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; uint8_t x_13; @@ -9485,7 +9485,7 @@ x_14 = lean_nat_add(x_2, x_3); x_15 = lean_unsigned_to_nat(2u); x_16 = lean_nat_div(x_14, x_15); lean_dec(x_14); -x_46 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6___closed__1; +x_46 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6___closed__1; x_47 = lean_array_get(x_46, x_1, x_16); x_48 = lean_array_get(x_46, x_1, x_2); x_49 = lean_ctor_get(x_47, 0); @@ -9512,7 +9512,7 @@ goto block_45; block_45: { lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; uint8_t x_23; -x_18 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6___closed__1; +x_18 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6___closed__1; x_19 = lean_array_get(x_18, x_17, x_3); x_20 = lean_array_get(x_18, x_17, x_2); x_21 = lean_ctor_get(x_19, 0); @@ -9538,7 +9538,7 @@ lean_object* x_27; lean_object* x_28; lean_dec(x_16); x_27 = l_Array_qsort_sort___at_Lean_registerParametricAttribute___spec__2___rarg___closed__1; lean_inc_n(x_2, 2); -x_28 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6(x_27, x_3, x_19, x_17, x_2, x_2); +x_28 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6(x_27, x_3, x_19, x_17, x_2, x_2); x_4 = x_28; goto block_12; } @@ -9551,7 +9551,7 @@ lean_dec(x_16); x_30 = lean_array_get(x_18, x_29, x_3); x_31 = l_Array_qsort_sort___at_Lean_registerParametricAttribute___spec__2___rarg___closed__1; lean_inc_n(x_2, 2); -x_32 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6(x_31, x_3, x_30, x_29, x_2, x_2); +x_32 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6(x_31, x_3, x_30, x_29, x_2, x_2); x_4 = x_32; goto block_12; } @@ -9578,7 +9578,7 @@ lean_object* x_39; lean_object* x_40; lean_dec(x_16); x_39 = l_Array_qsort_sort___at_Lean_registerParametricAttribute___spec__2___rarg___closed__1; lean_inc_n(x_2, 2); -x_40 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6(x_39, x_3, x_35, x_33, x_2, x_2); +x_40 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6(x_39, x_3, x_35, x_33, x_2, x_2); x_4 = x_40; goto block_12; } @@ -9591,7 +9591,7 @@ lean_dec(x_16); x_42 = lean_array_get(x_18, x_41, x_3); x_43 = l_Array_qsort_sort___at_Lean_registerParametricAttribute___spec__2___rarg___closed__1; lean_inc_n(x_2, 2); -x_44 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6(x_43, x_3, x_42, x_41, x_2, x_2); +x_44 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6(x_43, x_3, x_42, x_41, x_2, x_2); x_4 = x_44; goto block_12; } @@ -9610,7 +9610,7 @@ x_7 = lean_nat_dec_le(x_3, x_5); if (x_7 == 0) { lean_object* x_8; lean_object* x_9; lean_object* x_10; -x_8 = l_Array_qsort_sort___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__5(x_6, x_2, x_5); +x_8 = l_Array_qsort_sort___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__5(x_6, x_2, x_5); x_9 = lean_unsigned_to_nat(1u); x_10 = lean_nat_add(x_5, x_9); lean_dec(x_5); @@ -9627,7 +9627,7 @@ return x_6; } } } -uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__8(lean_object* x_1, lean_object* x_2, size_t x_3, size_t x_4) { +uint8_t l_Array_anyMUnsafe_any___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__8(lean_object* x_1, lean_object* x_2, size_t x_3, size_t x_4) { _start: { uint8_t x_5; @@ -9665,7 +9665,7 @@ return x_14; } } } -lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__7(lean_object* x_1, lean_object* x_2) { +lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__7(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; lean_object* x_4; uint8_t x_5; @@ -9710,7 +9710,7 @@ size_t x_16; size_t x_17; uint8_t x_18; x_16 = 0; x_17 = lean_usize_of_nat(x_8); lean_dec(x_8); -x_18 = l_Array_anyMUnsafe_any___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__8(x_1, x_6, x_16, x_17); +x_18 = l_Array_anyMUnsafe_any___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__8(x_1, x_6, x_16, x_17); lean_dec(x_6); if (x_18 == 0) { @@ -9781,7 +9781,7 @@ size_t x_39; size_t x_40; uint8_t x_41; x_39 = 0; x_40 = lean_usize_of_nat(x_31); lean_dec(x_31); -x_41 = l_Array_anyMUnsafe_any___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__8(x_1, x_29, x_39, x_40); +x_41 = l_Array_anyMUnsafe_any___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__8(x_1, x_29, x_39, x_40); lean_dec(x_29); if (x_41 == 0) { @@ -9815,31 +9815,31 @@ return x_52; } } } -lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3___lambda__1(lean_object* x_1) { +lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3___lambda__1(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; x_2 = l_Array_empty___closed__1; -x_3 = l_Std_RBNode_fold___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__4(x_2, x_1); +x_3 = l_Std_RBNode_fold___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__4(x_2, x_1); x_4 = lean_array_get_size(x_3); x_5 = lean_unsigned_to_nat(1u); x_6 = lean_nat_sub(x_4, x_5); lean_dec(x_4); x_7 = lean_unsigned_to_nat(0u); -x_8 = l_Array_qsort_sort___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__5(x_3, x_7, x_6); +x_8 = l_Array_qsort_sort___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__5(x_3, x_7, x_6); lean_dec(x_6); return x_8; } } -static lean_object* _init_l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3___closed__1() { +static lean_object* _init_l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3___closed__1() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3___lambda__1___boxed), 1, 0); +x_1 = lean_alloc_closure((void*)(l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3___lambda__1___boxed), 1, 0); return x_1; } } -lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3(lean_object* x_1, lean_object* x_2) { +lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; uint8_t x_4; @@ -9858,7 +9858,7 @@ lean_closure_set(x_8, 0, x_1); lean_closure_set(x_8, 1, x_7); x_9 = l_Lean_registerParametricAttribute___rarg___closed__1; x_10 = l_Lean_registerParametricAttribute___rarg___closed__2; -x_11 = l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3___closed__1; +x_11 = l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3___closed__1; x_12 = l_Lean_registerParametricAttribute___rarg___closed__3; lean_inc(x_5); x_13 = lean_alloc_ctor(0, 6, 0); @@ -9868,7 +9868,7 @@ lean_ctor_set(x_13, 2, x_8); lean_ctor_set(x_13, 3, x_10); lean_ctor_set(x_13, 4, x_11); lean_ctor_set(x_13, 5, x_12); -x_14 = l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__7(x_13, x_2); +x_14 = l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__7(x_13, x_2); if (lean_obj_tag(x_14) == 0) { lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; @@ -9986,7 +9986,7 @@ lean_closure_set(x_38, 0, x_1); lean_closure_set(x_38, 1, x_37); x_39 = l_Lean_registerParametricAttribute___rarg___closed__1; x_40 = l_Lean_registerParametricAttribute___rarg___closed__2; -x_41 = l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3___closed__1; +x_41 = l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3___closed__1; x_42 = l_Lean_registerParametricAttribute___rarg___closed__3; lean_inc(x_34); x_43 = lean_alloc_ctor(0, 6, 0); @@ -9996,7 +9996,7 @@ lean_ctor_set(x_43, 2, x_38); lean_ctor_set(x_43, 3, x_40); lean_ctor_set(x_43, 4, x_41); lean_ctor_set(x_43, 5, x_42); -x_44 = l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__7(x_43, x_2); +x_44 = l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__7(x_43, x_2); if (lean_obj_tag(x_44) == 0) { lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; @@ -10102,17 +10102,17 @@ return x_62; } } } -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__1(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* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__1(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___private_Lean_Meta_RecursorInfo_0__Lean_Meta_syntaxToMajorPos(x_2); -x_8 = l_Lean_ofExcept___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__1(x_7, x_3, x_4, x_5, x_6); +x_8 = l_Lean_ofExcept___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__1(x_7, x_3, x_4, x_5, x_6); lean_dec(x_7); return x_8; } } -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__2(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* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__2(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; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; @@ -10184,7 +10184,7 @@ return x_25; } } } -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; lean_object* x_5; @@ -10195,7 +10195,7 @@ lean_ctor_set(x_5, 1, x_3); return x_5; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__1() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__1() { _start: { lean_object* x_1; @@ -10203,17 +10203,17 @@ x_1 = lean_mk_string("recursor"); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__2() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__1; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__3() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__3() { _start: { lean_object* x_1; @@ -10221,12 +10221,12 @@ x_1 = lean_mk_string("user defined recursor, numerical parameter specifies posit return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__4() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__4() { _start: { lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; -x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__2; -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__3; +x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__2; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__3; x_3 = 0; x_4 = lean_alloc_ctor(0, 2, 1); lean_ctor_set(x_4, 0, x_1); @@ -10235,38 +10235,38 @@ lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_3); return x_4; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__5() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__5() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__1___boxed), 6, 0); +x_1 = lean_alloc_closure((void*)(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__1___boxed), 6, 0); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__6() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__6() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__2___boxed), 6, 0); +x_1 = lean_alloc_closure((void*)(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__2___boxed), 6, 0); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__7() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__7() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__3___boxed), 3, 0); +x_1 = lean_alloc_closure((void*)(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__3___boxed), 3, 0); return x_1; } } -static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__8() { +static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__4; -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__5; -x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__6; -x_4 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__7; +x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__4; +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__5; +x_3 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__6; +x_4 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__7; x_5 = lean_alloc_ctor(0, 4, 0); lean_ctor_set(x_5, 0, x_1); lean_ctor_set(x_5, 1, x_2); @@ -10275,31 +10275,31 @@ lean_ctor_set(x_5, 3, x_4); return x_5; } } -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069_(lean_object* x_1) { +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070_(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; -x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__8; -x_3 = l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3(x_2, x_1); +x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__8; +x_3 = l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3(x_2, x_1); return x_3; } } -lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__2___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +lean_object* l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__2___rarg___boxed(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; -x_6 = l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__2___rarg(x_1, x_2, x_3, x_4, x_5); +x_6 = l_Lean_throwError___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__2___rarg(x_1, x_2, x_3, x_4, x_5); lean_dec(x_4); lean_dec(x_3); lean_dec(x_2); return x_6; } } -lean_object* l_Lean_ofExcept___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +lean_object* l_Lean_ofExcept___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__1___boxed(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; -x_6 = l_Lean_ofExcept___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__1(x_1, x_2, x_3, x_4, x_5); +x_6 = l_Lean_ofExcept___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__1(x_1, x_2, x_3, x_4, x_5); lean_dec(x_4); lean_dec(x_3); lean_dec(x_2); @@ -10307,34 +10307,34 @@ lean_dec(x_1); return x_6; } } -lean_object* l_Std_RBNode_fold___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__4___boxed(lean_object* x_1, lean_object* x_2) { +lean_object* l_Std_RBNode_fold___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__4___boxed(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = l_Std_RBNode_fold___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__4(x_1, x_2); +x_3 = l_Std_RBNode_fold___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__4(x_1, x_2); lean_dec(x_2); return x_3; } } -lean_object* l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6___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) { +lean_object* l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6___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_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6(x_1, x_2, x_3, x_4, x_5, x_6); +x_7 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6(x_1, x_2, x_3, x_4, x_5, x_6); lean_dec(x_2); return x_7; } } -lean_object* l_Array_qsort_sort___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__5___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Array_qsort_sort___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__5___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; -x_4 = l_Array_qsort_sort___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__5(x_1, x_2, x_3); +x_4 = l_Array_qsort_sort___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__5(x_1, x_2, x_3); lean_dec(x_3); return x_4; } } -lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__8___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +lean_object* l_Array_anyMUnsafe_any___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__8___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { size_t x_5; size_t x_6; uint8_t x_7; lean_object* x_8; @@ -10342,27 +10342,27 @@ x_5 = lean_unbox_usize(x_3); lean_dec(x_3); x_6 = lean_unbox_usize(x_4); lean_dec(x_4); -x_7 = l_Array_anyMUnsafe_any___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__8(x_1, x_2, x_5, x_6); +x_7 = l_Array_anyMUnsafe_any___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__8(x_1, x_2, x_5, x_6); lean_dec(x_2); lean_dec(x_1); x_8 = lean_box(x_7); return x_8; } } -lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3___lambda__1___boxed(lean_object* x_1) { +lean_object* l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3___lambda__1___boxed(lean_object* x_1) { _start: { lean_object* x_2; -x_2 = l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3___lambda__1(x_1); +x_2 = l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3___lambda__1(x_1); lean_dec(x_1); return x_2; } } -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__1___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) { +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__1___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_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__1(x_1, x_2, x_3, x_4, x_5, x_6); +x_7 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__1(x_1, x_2, x_3, x_4, x_5, x_6); lean_dec(x_5); lean_dec(x_4); lean_dec(x_3); @@ -10371,20 +10371,20 @@ lean_dec(x_1); return x_7; } } -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__2___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) { +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__2___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_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__2(x_1, x_2, x_3, x_4, x_5, x_6); +x_7 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__2(x_1, x_2, x_3, x_4, x_5, x_6); lean_dec(x_3); return x_7; } } -lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; -x_4 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____lambda__3(x_1, x_2, x_3); +x_4 = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____lambda__3(x_1, x_2, x_3); lean_dec(x_2); lean_dec(x_1); return x_4; @@ -10410,7 +10410,7 @@ x_7 = lean_nat_add(x_3, x_4); x_8 = lean_unsigned_to_nat(2u); x_9 = lean_nat_div(x_7, x_8); lean_dec(x_7); -x_10 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6___closed__1; +x_10 = l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6___closed__1; x_11 = lean_array_get(x_10, x_1, x_9); x_12 = lean_ctor_get(x_11, 0); lean_inc(x_12); @@ -10877,27 +10877,27 @@ l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_syntaxToMajorPos___closed__3 = _ lean_mark_persistent(l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_syntaxToMajorPos___closed__3); l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_syntaxToMajorPos___closed__4 = _init_l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_syntaxToMajorPos___closed__4(); lean_mark_persistent(l___private_Lean_Meta_RecursorInfo_0__Lean_Meta_syntaxToMajorPos___closed__4); -l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6___closed__1 = _init_l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6___closed__1(); -lean_mark_persistent(l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__6___closed__1); -l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3___closed__1 = _init_l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3___closed__1(); -lean_mark_persistent(l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____spec__3___closed__1); -l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__1(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__1); -l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__2(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__2); -l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__3(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__3); -l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__4(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__4); -l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__5 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__5(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__5); -l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__6 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__6(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__6); -l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__7 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__7(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__7); -l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__8 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__8(); -lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069____closed__8); -res = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2069_(lean_io_mk_world()); +l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6___closed__1 = _init_l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6___closed__1(); +lean_mark_persistent(l_Array_qpartition_loop___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__6___closed__1); +l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3___closed__1 = _init_l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3___closed__1(); +lean_mark_persistent(l_Lean_registerParametricAttribute___at_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____spec__3___closed__1); +l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__1(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__1); +l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__2(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__2); +l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__3(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__3); +l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__4(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__4); +l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__5 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__5(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__5); +l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__6 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__6(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__6); +l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__7 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__7(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__7); +l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__8 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__8(); +lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070____closed__8); +res = l_Lean_Meta_initFn____x40_Lean_Meta_RecursorInfo___hyg_2070_(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; l_Lean_Meta_recursorAttribute = lean_io_result_get_value(res); lean_mark_persistent(l_Lean_Meta_recursorAttribute);