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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-03 11:17:35 -08:00
parent 137c70f055
commit 35c587afbf
20 changed files with 14354 additions and 9912 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
stage0/src/Lean/Elab/PreDefinition/WF/Main.lean generated
View file

@ -88,18 +88,18 @@ def wfRecursion (preDefs : Array PreDefinition) (wf? : Option TerminationWF) (de
return (← packMutual fixedPrefixSize unaryPreDefs, fixedPrefixSize)
let preDefNonRec ← forallBoundedTelescope unaryPreDef.type fixedPrefixSize fun prefixArgs type => do
let packedArgType := type.bindingDomain!
let wfRel ← elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType wf?
trace[Elab.definition.wf] "wfRel: {wfRel}"
let (value, envNew) ← withoutModifyingEnv' do
addAsAxiom unaryPreDef
let value ← mkFix unaryPreDef prefixArgs wfRel decrTactic?
eraseRecAppSyntaxExpr value
/- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
let value ← unfoldDeclsFrom envNew value
return { unaryPreDef with value }
elabWFRel preDefs unaryPreDef.declName fixedPrefixSize packedArgType wf? fun wfRel => do
trace[Elab.definition.wf] "wfRel: {wfRel}"
let (value, envNew) ← withoutModifyingEnv' do
addAsAxiom unaryPreDef
let value ← mkFix unaryPreDef prefixArgs wfRel decrTactic?
eraseRecAppSyntaxExpr value
/- `mkFix` invokes `decreasing_tactic` which may add auxiliary theorems to the environment. -/
let value ← unfoldDeclsFrom envNew value
return { unaryPreDef with value }
trace[Elab.definition.wf] ">> {preDefNonRec.declName} :=\n{preDefNonRec.value}"
let preDefs ← preDefs.mapM fun d => eraseRecAppSyntax d
addNonRec preDefNonRec
addNonRec preDefNonRec (applyAttrAfterCompilation := false)
addNonRecPreDefs preDefs preDefNonRec fixedPrefixSize
registerEqnsInfo preDefs preDefNonRec.declName
for preDef in preDefs do

113
stage0/src/Lean/Elab/PreDefinition/WF/Rel.lean generated
View file

@ -53,7 +53,52 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva
rename mvarId fvarId varNames.back
go 0 mvarId fvarId
def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPrefixSize : Nat) (argType : Expr) (wf? : Option TerminationWF) : TermElabM Expr := do
def getNumCandidateArgs (fixedPrefixSize : Nat) (preDefs : Array PreDefinition) : MetaM (Array Nat) := do
preDefs.mapM fun preDef =>
lambdaTelescope preDef.value fun xs _ =>
return xs.size - fixedPrefixSize
/--
Given a predefinition with value `fun (x_₁ ... xₙ) (y_₁ : α₁)... (yₘ : αₘ) => ...`,
where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff `sizeOf yᵢ` reduces to a literal.
This is the case for types such as `Prop`, `Type u`, etc.
This arguments should not be considered when guessing a well-founded relation.
See `generateCombinations?`
-/
def getForbiddenByTrivialSizeOf (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) :=
lambdaTelescope preDef.value fun xs _ => do
let mut result := #[]
for x in xs[fixedPrefixSize:], i in [:xs.size] do
try
let sizeOf ← whnfD (← mkAppM ``sizeOf #[x])
if sizeOf.isLit then
result := result.push i
catch _ =>
result := result.push i
return result
def generateCombinations? (forbiddenArgs : Array (Array Nat)) (numArgs : Array Nat) (threshold : Nat := 32) : Option (Array (Array Nat)) :=
go 0 #[] |>.run #[] |>.2
where
isForbidden (fidx : Nat) (argIdx : Nat) : Bool :=
if h : fidx < forbiddenArgs.size then
forbiddenArgs.get ⟨fidx, h⟩ |>.contains argIdx
else
false
go (fidx : Nat) : OptionT (ReaderT (Array Nat) (StateM (Array (Array Nat)))) Unit := do
if h : fidx < numArgs.size then
let n := numArgs.get ⟨fidx, h⟩
for argIdx in [:n] do
unless isForbidden fidx argIdx do
withReader (·.push argIdx) (go (fidx + 1))
else
modify (·.push (← read))
if (← get).size > threshold then
failure
termination_by _ fidx => numArgs.size - fidx
def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPrefixSize : Nat) (argType : Expr) (wf? : Option TerminationWF) (k : Expr → TermElabM α) : TermElabM α := do
let α := argType
let u ← getLevel α
let expectedType := mkApp (mkConst ``WellFoundedRelation [u]) α
@ -63,22 +108,54 @@ def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPre
let wfRel ← instantiateMVars (← withSynthesize <| elabTermEnsuringType wfStx expectedType)
let pendingMVarIds ← getMVars wfRel
discard <| logUnassignedUsingErrorInfos pendingMVarIds
return wfRel
| some (TerminationWF.ext elements) => withDeclName unaryPreDefName <| withRef (getRefFromElems elements) do
let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
let [fMVarId, wfRelMVarId, _] ← apply mainMVarId (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
let (d, fMVarId) ← intro1 fMVarId
let subgoals ← unpackMutual preDefs fMVarId d
for (d, mvarId) in subgoals, element in elements, preDef in preDefs do
let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
withMVarContext mvarId do
let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← getMVarType mvarId)
assignExprMVar mvarId value
let wfRelVal ← synthInstance (← inferType (mkMVar wfRelMVarId))
assignExprMVar wfRelMVarId wfRelVal
instantiateMVars (mkMVar mainMVarId)
| none =>
-- TODO: try to synthesize some default relation
throwError "'termination_by' modifier missing"
k wfRel
| some (TerminationWF.ext elements) => go expectedType elements
| none => guess expectedType
where
go (expectedType : Expr) (elements : Array TerminationByElement) : TermElabM α :=
withDeclName unaryPreDefName <| withRef (getRefFromElems elements) do
let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
let [fMVarId, wfRelMVarId, _] ← apply mainMVarId (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
let (d, fMVarId) ← intro1 fMVarId
let subgoals ← unpackMutual preDefs fMVarId d
for (d, mvarId) in subgoals, element in elements, preDef in preDefs do
let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
withMVarContext mvarId do
let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← getMVarType mvarId)
assignExprMVar mvarId value
let wfRelVal ← synthInstance (← inferType (mkMVar wfRelMVarId))
assignExprMVar wfRelMVarId wfRelVal
k (← instantiateMVars (mkMVar mainMVarId))
generateElements (numArgs : Array Nat) (argCombination : Array Nat) : TermElabM (Array TerminationByElement) := do
let mut result := #[]
let var ← `(x)
let body ← `(sizeOf x)
let hole ← `(_)
for preDef in preDefs, numArg in numArgs, argIdx in argCombination do
let mut vars := #[var]
for i in [:numArg - argIdx - 1] do
vars := vars.push hole
result := result.push {
ref := preDef.ref
declName := preDef.declName
vars := vars
body := body
implicit := false
}
return result
guess (expectedType : Expr) : TermElabM α := do
-- TODO: add support for lex
let numArgs ← getNumCandidateArgs fixedPrefixSize preDefs
-- TODO: include in `forbiddenArgs` arguments that are fixed but are not in the fixed prefix
let forbiddenArgs ← preDefs.mapM fun preDef => getForbiddenByTrivialSizeOf fixedPrefixSize preDef
-- TODO: add option to control the maximum number of cases to try
if let some combs := generateCombinations? forbiddenArgs numArgs then
for comb in combs do
let elements ← generateElements numArgs comb
if let some r ← observing? (go expectedType elements) then
return r
throwError "failed to prove termination, use `termination_by` to specify a well-founded relation"
end Lean.Elab.WF

33
stage0/src/Lean/Meta/Tactic/LinearArith/Basic.lean generated Normal file
View file

@ -0,0 +1,33 @@
/-
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Expr
namespace Lean.Meta.Linear
/-- Quick filter for linear terms. -/
def isLinearTerm (e : Expr) : Bool :=
let f := e.getAppFn
if !f.isConst then
false
else
let n := f.constName!
n == ``HAdd.hAdd || n == ``HMul.hMul || n == ``HSub.hSub || n == ``Nat.succ
/-- Quick filter for linear constraints. -/
partial def isLinearCnstr (e : Expr) : Bool :=
let f := e.getAppFn
if !f.isConst then
false
else
let n := f.constName!
if n == ``Eq || n == ``LT.lt || n == ``LE.le || n == ``GT.gt || n == ``GE.ge || n == ``Ne then
true
else if n == ``Not && e.getAppNumArgs == 1 then
isLinearCnstr e.appArg!
else
false
end Lean.Meta.Linear

215
stage0/src/Lean/Meta/Tactic/LinearArith/Nat.lean generated
View file

@ -3,216 +3,5 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Check
import Lean.Meta.Offset
import Lean.Meta.KExprMap
namespace Lean.Meta.Linear.Nat
deriving instance Repr for Nat.Linear.Expr
abbrev LinearExpr := Nat.Linear.Expr
abbrev LinearCnstr := Nat.Linear.ExprCnstr
abbrev PolyExpr := Nat.Linear.Poly
def LinearExpr.toExpr (e : LinearExpr) : Expr :=
open Nat.Linear.Expr in
match e with
| num v => mkApp (mkConst ``num) (mkNatLit v)
| var i => mkApp (mkConst ``var) (mkNatLit i)
| add a b => mkApp2 (mkConst ``add) (toExpr a) (toExpr b)
| mulL k a => mkApp2 (mkConst ``mulL) (mkNatLit k) (toExpr a)
| mulR a k => mkApp2 (mkConst ``mulL) (toExpr a) (mkNatLit k)
instance : ToExpr LinearExpr where
toExpr a := a.toExpr
toTypeExpr := mkConst ``Nat.Linear.Expr
protected def LinearCnstr.toExpr (c : LinearCnstr) : Expr :=
mkApp3 (mkConst ``Nat.Linear.ExprCnstr.mk) (toExpr c.eq) (LinearExpr.toExpr c.lhs) (LinearExpr.toExpr c.rhs)
instance : ToExpr LinearCnstr where
toExpr a := a.toExpr
toTypeExpr := mkConst ``Nat.Linear.ExprCnstr
open Nat.Linear.Expr in
def LinearExpr.toArith (ctx : Array Expr) (e : LinearExpr) : MetaM Expr := do
match e with
| num v => return mkNatLit v
| var i => return ctx[i]
| add a b => mkAdd (← toArith ctx a) (← toArith ctx b)
| mulL k a => mkMul (mkNatLit k) (← toArith ctx a)
| mulR a k => mkMul (← toArith ctx a) (mkNatLit k)
def LinearCnstr.toArith (ctx : Array Expr) (c : LinearCnstr) : MetaM Expr := do
if c.eq then
mkEq (← LinearExpr.toArith ctx c.lhs) (← LinearExpr.toArith ctx c.rhs)
else
return mkApp4 (mkConst ``LE.le [levelZero]) (mkConst ``Nat) (mkConst ``instLENat) (← LinearExpr.toArith ctx c.lhs) (← LinearExpr.toArith ctx c.rhs)
namespace ToLinear
structure State where
varMap : KExprMap Nat := {} -- It should be fine to use `KExprMap` here because the mapping should be small and few HeadIndex collisions.
vars : Array Expr := #[]
abbrev M := StateRefT State MetaM
open Nat.Linear.Expr
def addAsVar (e : Expr) : M LinearExpr := do
if let some x ← (← get).varMap.find? e then
return var x
else
let x := (← get).vars.size
let s ← get
set { varMap := (← s.varMap.insert e x), vars := s.vars.push e : State }
return var x
partial def toLinearExpr (e : Expr) : M LinearExpr := do
match e with
| Expr.lit (Literal.natVal n) _ => return num n
| Expr.mdata _ e _ => toLinearExpr e
| Expr.const ``Nat.zero .. => return num 0
| Expr.app .. => visit e
| Expr.mvar .. => visit e
| _ => addAsVar e
where
visit (e : Expr) : M LinearExpr := do
let f := e.getAppFn
match f with
| Expr.mvar .. =>
let eNew ← instantiateMVars e
if eNew != e then
toLinearExpr eNew
else
addAsVar e
| Expr.const declName .. =>
let numArgs := e.getAppNumArgs
if declName == ``Nat.succ && numArgs == 1 then
return inc (← toLinearExpr e.appArg!)
else if declName == ``Nat.add && numArgs == 2 then
return add (← toLinearExpr (e.getArg! 0)) (← toLinearExpr (e.getArg! 1))
else if declName == ``Nat.mul && numArgs == 2 then
match (← evalNat (e.getArg! 0) |>.run) with
| some k => return mulL k (← toLinearExpr (e.getArg! 1))
| none => match (← evalNat (e.getArg! 1) |>.run) with
| some k => return mulR (← toLinearExpr (e.getArg! 0)) k
| none => addAsVar e
else if isNatProjInst declName numArgs then
if let some e ← unfoldProjInst? e then
toLinearExpr e
else
addAsVar e
else
addAsVar e
| _ => addAsVar e
partial def toLinearCnstr? (e : Expr) : M (Option LinearCnstr) := do
let f := e.getAppFn
match f with
| Expr.mvar .. =>
let eNew ← instantiateMVars e
if eNew != e then
toLinearCnstr? eNew
else
return none
| Expr.const declName .. =>
let numArgs := e.getAppNumArgs
if declName == ``Eq && numArgs == 3 then
return some { eq := true, lhs := (← toLinearExpr (e.getArg! 1)), rhs := (← toLinearExpr (e.getArg! 2)) }
else if declName == ``Nat.le && numArgs == 2 then
return some { eq := false, lhs := (← toLinearExpr (e.getArg! 0)), rhs := (← toLinearExpr (e.getArg! 1)) }
else if declName == ``Nat.lt && numArgs == 2 then
return some { eq := false, lhs := (← toLinearExpr (e.getArg! 0)).inc, rhs := (← toLinearExpr (e.getArg! 1)) }
else if numArgs == 4 && (declName == ``GE.ge || declName == ``GT.gt) then
if let some e ← unfoldDefinition? e then
toLinearCnstr? e
else
return none
else if numArgs == 4 && (declName == ``LE.le || declName == ``LT.lt) then
if (← isDefEq (e.getArg! 0) (mkConst ``Nat)) then
if let some e ← unfoldProjInst? e then
toLinearCnstr? e
else
return none
else
return none
else
return none
| _ => return none
def run (x : M α) : MetaM (α × Array Expr) := do
let (a, s) ← x.run {}
return (a, s.vars)
end ToLinear
open ToLinear (toLinearCnstr? toLinearExpr)
def toContextExpr (ctx : Array Expr) : MetaM Expr := do
mkListLit (mkConst ``Nat) ctx.toList
def reflTrue : Expr :=
mkApp2 (mkConst ``Eq.refl [levelOne]) (mkConst ``Bool) (mkConst ``Bool.true)
def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
let (some c, ctx) ← ToLinear.run (ToLinear.toLinearCnstr? e) | return none
let c₁ := c.toPoly
let c₂ := c₁.norm
if c₂.isUnsat then
let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (← toContextExpr ctx) (toExpr c) reflTrue
return some (mkConst ``False, p)
else if c₂.isValid then
let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (← toContextExpr ctx) (toExpr c) reflTrue
return some (mkConst ``True, p)
else if c₁ != c₂ then
let c₂ : LinearCnstr := c₂.toExpr
let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
let r ← c₂.toArith ctx
return some (r, p)
else
return none
def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
if let some arg := e.not? then
let mut eNew? := none
let mut thmName := Name.anonymous
if arg.isAppOfArity ``LE.le 4 then
eNew? := some (← mkLE (← mkAdd (arg.getArg! 3) (mkNatLit 1)) (arg.getArg! 2))
thmName := ``Nat.not_le_eq
else if arg.isAppOfArity ``GE.ge 4 then
eNew? := some (← mkLE (← mkAdd (arg.getArg! 2) (mkNatLit 1)) (arg.getArg! 3))
thmName := ``Nat.not_ge_eq
else if arg.isAppOfArity ``LT.lt 4 then
eNew? := some (← mkLE (arg.getArg! 3) (arg.getArg! 2))
thmName := ``Nat.not_lt_eq
else if arg.isAppOfArity ``GT.gt 4 then
eNew? := some (← mkLE (arg.getArg! 2) (arg.getArg! 3))
thmName := ``Nat.not_gt_eq
if let some eNew := eNew? then
let h₁ := mkApp2 (mkConst thmName) (arg.getArg! 2) (arg.getArg! 3)
if let some (eNew', h₂) ← simpCnstrPos? eNew then
let h := mkApp6 (mkConst ``Eq.trans [levelOne]) (mkSort levelZero) e eNew eNew' h₁ h₂
return some (eNew', h)
else
return some (eNew, h₁)
else
return none
else
simpCnstrPos? e
def simpExpr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
let (e, ctx) ← ToLinear.run (ToLinear.toLinearExpr e)
let p := e.toPoly
let p' := p.norm
if p'.length < p.length then
-- We only return some if monomials were fused
let e' : LinearExpr := p'.toExpr
let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr e) (toExpr e') reflTrue
let r ← e'.toArith ctx
return some (r, p)
else
return none
end Lean.Meta.Linear.Nat
import Lean.Meta.Tactic.LinearArith.Nat.Basic
import Lean.Meta.Tactic.LinearArith.Nat.Simp

159
stage0/src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean generated Normal file
View file

@ -0,0 +1,159 @@
/-
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Check
import Lean.Meta.Offset
import Lean.Meta.KExprMap
namespace Lean.Meta.Linear.Nat
deriving instance Repr for Nat.Linear.Expr
abbrev LinearExpr := Nat.Linear.Expr
abbrev LinearCnstr := Nat.Linear.ExprCnstr
abbrev PolyExpr := Nat.Linear.Poly
def LinearExpr.toExpr (e : LinearExpr) : Expr :=
open Nat.Linear.Expr in
match e with
| num v => mkApp (mkConst ``num) (mkNatLit v)
| var i => mkApp (mkConst ``var) (mkNatLit i)
| add a b => mkApp2 (mkConst ``add) (toExpr a) (toExpr b)
| mulL k a => mkApp2 (mkConst ``mulL) (mkNatLit k) (toExpr a)
| mulR a k => mkApp2 (mkConst ``mulL) (toExpr a) (mkNatLit k)
instance : ToExpr LinearExpr where
toExpr a := a.toExpr
toTypeExpr := mkConst ``Nat.Linear.Expr
protected def LinearCnstr.toExpr (c : LinearCnstr) : Expr :=
mkApp3 (mkConst ``Nat.Linear.ExprCnstr.mk) (toExpr c.eq) (LinearExpr.toExpr c.lhs) (LinearExpr.toExpr c.rhs)
instance : ToExpr LinearCnstr where
toExpr a := a.toExpr
toTypeExpr := mkConst ``Nat.Linear.ExprCnstr
open Nat.Linear.Expr in
def LinearExpr.toArith (ctx : Array Expr) (e : LinearExpr) : MetaM Expr := do
match e with
| num v => return mkNatLit v
| var i => return ctx[i]
| add a b => mkAdd (← toArith ctx a) (← toArith ctx b)
| mulL k a => mkMul (mkNatLit k) (← toArith ctx a)
| mulR a k => mkMul (← toArith ctx a) (mkNatLit k)
def LinearCnstr.toArith (ctx : Array Expr) (c : LinearCnstr) : MetaM Expr := do
if c.eq then
mkEq (← LinearExpr.toArith ctx c.lhs) (← LinearExpr.toArith ctx c.rhs)
else
return mkApp4 (mkConst ``LE.le [levelZero]) (mkConst ``Nat) (mkConst ``instLENat) (← LinearExpr.toArith ctx c.lhs) (← LinearExpr.toArith ctx c.rhs)
namespace ToLinear
structure State where
varMap : KExprMap Nat := {} -- It should be fine to use `KExprMap` here because the mapping should be small and few HeadIndex collisions.
vars : Array Expr := #[]
abbrev M := StateRefT State MetaM
open Nat.Linear.Expr
def addAsVar (e : Expr) : M LinearExpr := do
if let some x ← (← get).varMap.find? e then
return var x
else
let x := (← get).vars.size
let s ← get
set { varMap := (← s.varMap.insert e x), vars := s.vars.push e : State }
return var x
partial def toLinearExpr (e : Expr) : M LinearExpr := do
match e with
| Expr.lit (Literal.natVal n) _ => return num n
| Expr.mdata _ e _ => toLinearExpr e
| Expr.const ``Nat.zero .. => return num 0
| Expr.app .. => visit e
| Expr.mvar .. => visit e
| _ => addAsVar e
where
visit (e : Expr) : M LinearExpr := do
let f := e.getAppFn
match f with
| Expr.mvar .. =>
let eNew ← instantiateMVars e
if eNew != e then
toLinearExpr eNew
else
addAsVar e
| Expr.const declName .. =>
let numArgs := e.getAppNumArgs
if declName == ``Nat.succ && numArgs == 1 then
return inc (← toLinearExpr e.appArg!)
else if declName == ``Nat.add && numArgs == 2 then
return add (← toLinearExpr (e.getArg! 0)) (← toLinearExpr (e.getArg! 1))
else if declName == ``Nat.mul && numArgs == 2 then
match (← evalNat (e.getArg! 0) |>.run) with
| some k => return mulL k (← toLinearExpr (e.getArg! 1))
| none => match (← evalNat (e.getArg! 1) |>.run) with
| some k => return mulR (← toLinearExpr (e.getArg! 0)) k
| none => addAsVar e
else if isNatProjInst declName numArgs then
if let some e ← unfoldProjInst? e then
toLinearExpr e
else
addAsVar e
else
addAsVar e
| _ => addAsVar e
partial def toLinearCnstr? (e : Expr) : M (Option LinearCnstr) := do
let f := e.getAppFn
match f with
| Expr.mvar .. =>
let eNew ← instantiateMVars e
if eNew != e then
toLinearCnstr? eNew
else
return none
| Expr.const declName .. =>
let numArgs := e.getAppNumArgs
if declName == ``Eq && numArgs == 3 then
return some { eq := true, lhs := (← toLinearExpr (e.getArg! 1)), rhs := (← toLinearExpr (e.getArg! 2)) }
else if declName == ``Nat.le && numArgs == 2 then
return some { eq := false, lhs := (← toLinearExpr (e.getArg! 0)), rhs := (← toLinearExpr (e.getArg! 1)) }
else if declName == ``Nat.lt && numArgs == 2 then
return some { eq := false, lhs := (← toLinearExpr (e.getArg! 0)).inc, rhs := (← toLinearExpr (e.getArg! 1)) }
else if numArgs == 4 && (declName == ``GE.ge || declName == ``GT.gt) then
if let some e ← unfoldDefinition? e then
toLinearCnstr? e
else
return none
else if numArgs == 4 && (declName == ``LE.le || declName == ``LT.lt) then
if (← isDefEq (e.getArg! 0) (mkConst ``Nat)) then
if let some e ← unfoldProjInst? e then
toLinearCnstr? e
else
return none
else
return none
else
return none
| _ => return none
def run (x : M α) : MetaM (α × Array Expr) := do
let (a, s) ← x.run {}
return (a, s.vars)
end ToLinear
export ToLinear (toLinearCnstr? toLinearExpr)
def toContextExpr (ctx : Array Expr) : MetaM Expr := do
mkListLit (mkConst ``Nat) ctx.toList
def reflTrue : Expr :=
mkApp2 (mkConst ``Eq.refl [levelOne]) (mkConst ``Bool) (mkConst ``Bool.true)
namespace Lean.Meta.Linear.Nat

69
stage0/src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean generated Normal file
View file

@ -0,0 +1,69 @@
/-
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Tactic.LinearArith.Nat.Basic
namespace Lean.Meta.Linear.Nat
def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
let (some c, ctx) ← ToLinear.run (ToLinear.toLinearCnstr? e) | return none
let c₁ := c.toPoly
let c₂ := c₁.norm
if c₂.isUnsat then
let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (← toContextExpr ctx) (toExpr c) reflTrue
return some (mkConst ``False, p)
else if c₂.isValid then
let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (← toContextExpr ctx) (toExpr c) reflTrue
return some (mkConst ``True, p)
else if c₁ != c₂ then
let c₂ : LinearCnstr := c₂.toExpr
let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
let r ← c₂.toArith ctx
return some (r, p)
else
return none
def simpCnstr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
if let some arg := e.not? then
let mut eNew? := none
let mut thmName := Name.anonymous
if arg.isAppOfArity ``LE.le 4 then
eNew? := some (← mkLE (← mkAdd (arg.getArg! 3) (mkNatLit 1)) (arg.getArg! 2))
thmName := ``Nat.not_le_eq
else if arg.isAppOfArity ``GE.ge 4 then
eNew? := some (← mkLE (← mkAdd (arg.getArg! 2) (mkNatLit 1)) (arg.getArg! 3))
thmName := ``Nat.not_ge_eq
else if arg.isAppOfArity ``LT.lt 4 then
eNew? := some (← mkLE (arg.getArg! 3) (arg.getArg! 2))
thmName := ``Nat.not_lt_eq
else if arg.isAppOfArity ``GT.gt 4 then
eNew? := some (← mkLE (arg.getArg! 2) (arg.getArg! 3))
thmName := ``Nat.not_gt_eq
if let some eNew := eNew? then
let h₁ := mkApp2 (mkConst thmName) (arg.getArg! 2) (arg.getArg! 3)
if let some (eNew', h₂) ← simpCnstrPos? eNew then
let h := mkApp6 (mkConst ``Eq.trans [levelOne]) (mkSort levelZero) e eNew eNew' h₁ h₂
return some (eNew', h)
else
return some (eNew, h₁)
else
return none
else
simpCnstrPos? e
def simpExpr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
let (e, ctx) ← ToLinear.run (ToLinear.toLinearExpr e)
let p := e.toPoly
let p' := p.norm
if p'.length < p.length then
-- We only return some if monomials were fused
let e' : LinearExpr := p'.toExpr
let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr e) (toExpr e') reflTrue
let r ← e'.toArith ctx
return some (r, p)
else
return none
end Lean.Meta.Linear.Nat

26
stage0/src/Lean/Meta/Tactic/LinearArith/Nat/Solver.lean generated Normal file
View file

@ -0,0 +1,26 @@
/-
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Tactic.LinearArith.Solver
import Lean.Meta.Tactic.LinearArith.Nat.Basic
namespace Lean.Meta.Linear.Nat
namespace Collect
structure Cnstr where
cnstr : LinearArith
proof : Expr
structure State where
cnstrs : Array Cnstr
abbrev M := StateRefT State ToLinear.M
-- TODO
end Collect
end Lean.Meta.Linear.Nat

32
stage0/src/Lean/Meta/Tactic/LinearArith/Simp.lean generated
View file

@ -3,43 +3,21 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Tactic.LinearArith.Nat
import Lean.Meta.Tactic.LinearArith.Basic
import Lean.Meta.Tactic.LinearArith.Nat.Simp
namespace Lean.Meta.Linear
/-- Quick filter simpExpr? -/
private partial def isSimpExprTarget (e : Expr) : Bool :=
let f := e.getAppFn
if !f.isConst then
false
else
let n := f.constName!
n == ``HAdd.hAdd || n == ``HMul.hMul || n == ``HSub.hSub || n == ``Nat.succ
/-- Quick filter simpCnstr? -/
private partial def isSimpCnstrTarget (e : Expr) : Bool :=
let f := e.getAppFn
if !f.isConst then
false
else
let n := f.constName!
if n == ``Eq || n == ``LT.lt || n == ``LE.le || n == ``GT.gt || n == ``GE.ge then
true
else if n == ``Not && e.getAppNumArgs == 1 then
isSimpCnstrTarget e.appArg!
else
false
private def parentIsTarget (parent? : Option Expr) : Bool :=
match parent? with
| none => false
| some parent => isSimpExprTarget parent || isSimpCnstrTarget parent
| some parent => isLinearTerm parent || isLinearCnstr parent
def simp? (e : Expr) (parent? : Option Expr) : MetaM (Option (Expr × Expr)) := do
-- TODO: add support for `Int` and arbitrary ordered comm rings
if isSimpCnstrTarget e then
if isLinearCnstr e then
Nat.simpCnstr? e
else if isSimpExprTarget e && !parentIsTarget parent? then
else if isLinearTerm e && !parentIsTarget parent? then
trace[Meta.Tactic.simp] "arith expr: {e}"
Nat.simpExpr? e
else

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

@ -1678,7 +1678,7 @@ def checkNoImmediateColon : Parser := {
def setExpectedFn (expected : List String) (p : ParserFn) : ParserFn := fun c s =>
match p c s with
| s'@{ errorMsg := some msg, .. } => { s' with errorMsg := some { msg with expected := [] } }
| s'@{ errorMsg := some msg, .. } => { s' with errorMsg := some { msg with expected } }
| s' => s'
def setExpected (expected : List String) (p : Parser) : Parser :=

8
stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean generated
View file

@ -686,6 +686,14 @@ where
| none => withBindingBodyUnusedName fun h => do
return (← delab, h.getId)
@[builtinDelab app.cond]
def delabCond : Delab := whenPPOption getPPNotation do
guard $ (← getExpr).getAppNumArgs == 4
let c ← withAppFn $ withAppFn $ withAppArg delab
let t ← withAppFn $ withAppArg delab
let e ← withAppArg delab
`(bif $c then $t else $e)
@[builtinDelab app.namedPattern]
def delabNamedPattern : Delab := do
-- Note: we keep this as a delaborator because it accesses the DelabM context

416
stage0/stdlib/Lean/Elab/PreDefinition/WF/Main.c generated
View file

@ -35,7 +35,7 @@ lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
static lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs___spec__1___lambda__2___closed__1;
static lean_object* l_Lean_Elab_wfRecursion___closed__6;
static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs_mkSum___spec__1___closed__11;
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___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*);
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___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*, lean_object*, lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_getFixedPrefix___spec__3___lambda__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*);
uint8_t lean_name_eq(lean_object*, lean_object*);
@ -52,11 +52,12 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_getFixedPrefix_
LEAN_EXPORT lean_object* l_Lean_Elab_withCommonTelescope_go___rarg___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* lean_string_append(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_getFixedPrefix___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_getFixedPrefix___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*);
static lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs___spec__1___closed__6;
LEAN_EXPORT lean_object* l_Lean_Elab_getFixedPrefix(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_WF_packMutual(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_withCommonTelescope(lean_object*);
lean_object* l_panic___at___private_Lean_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_processPSigmaCasesOn___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_wfRecursion___lambda__1___closed__2;
@ -98,8 +99,8 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Ela
lean_object* l_Lean_Elab_WF_registerEqnsInfo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_repr(lean_object*);
lean_object* lean_st_mk_ref(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__3(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_PreDefinition_WF_Main___hyg_2032_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__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*);
LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_PreDefinition_WF_Main___hyg_2027_(lean_object*);
static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs_mkSum___spec__1___closed__10;
static lean_object* l_Lean_Elab_wfRecursion___closed__5;
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs___spec__1___lambda__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*, lean_object*, lean_object*);
@ -120,7 +121,6 @@ lean_object* l_Lean_Core_transform___at_Lean_Core_betaReduce___spec__1(lean_obje
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___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_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_getFixedPrefix___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*, lean_object*);
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_Elab_getFixedPrefix___spec__1(lean_object*, lean_object*, size_t, size_t);
lean_object* l_Lean_Elab_WF_elabWFRel(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Lean_Elab_addAndCompilePartialRec(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs_mkSum(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -136,10 +136,11 @@ LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_getFixedPrefix___
lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs(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_WF_elabWFRel___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*, lean_object*);
static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs_mkSum___spec__1___closed__3;
lean_object* l_Lean_Expr_bindingName_x21(lean_object*);
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__4(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_isOnlyOneUnaryDef___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_wfRecursion___closed__2;
@ -158,7 +159,7 @@ static lean_object* l_Lean_Elab_wfRecursion___lambda__2___closed__2;
static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs_mkSum___spec__1___closed__9;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_wfRecursion___lambda__2___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__4___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_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs___spec__1___lambda__1___closed__2;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_getFixedPrefix___spec__2(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -195,6 +196,7 @@ static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_PreDefinitio
static lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs_mkSum___spec__1___closed__1;
lean_object* l_Lean_Elab_WF_packDomain(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Expr_withAppAux___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs_mkSum___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_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_isOnlyOneUnaryDef___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) {
_start:
@ -4304,139 +4306,103 @@ x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___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* x_13, lean_object* x_14, lean_object* x_15) {
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___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* x_13) {
_start:
{
lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_16 = l_Lean_Expr_bindingDomain_x21(x_8);
lean_dec(x_8);
x_17 = lean_ctor_get(x_1, 3);
lean_inc(x_17);
lean_inc(x_14);
lean_inc(x_13);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_17);
x_18 = l_Lean_Elab_WF_elabWFRel(x_2, x_17, x_3, x_16, x_4, x_9, x_10, x_11, x_12, x_13, x_14, x_15);
if (lean_obj_tag(x_18) == 0)
lean_object* x_14; uint8_t x_15; lean_object* x_16; lean_object* x_29; lean_object* x_30; lean_object* x_31; uint8_t x_32;
x_14 = l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs___spec__1___closed__6;
x_29 = lean_st_ref_get(x_12, x_13);
x_30 = lean_ctor_get(x_29, 0);
lean_inc(x_30);
x_31 = lean_ctor_get(x_30, 3);
lean_inc(x_31);
lean_dec(x_30);
x_32 = lean_ctor_get_uint8(x_31, sizeof(void*)*1);
lean_dec(x_31);
if (x_32 == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23; lean_object* x_36; lean_object* x_37; lean_object* x_38; uint8_t x_39;
x_19 = lean_ctor_get(x_18, 0);
lean_inc(x_19);
x_20 = lean_ctor_get(x_18, 1);
lean_inc(x_20);
lean_dec(x_18);
x_21 = l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs___spec__1___closed__6;
x_36 = lean_st_ref_get(x_14, x_20);
lean_object* x_33; uint8_t x_34;
x_33 = lean_ctor_get(x_29, 1);
lean_inc(x_33);
lean_dec(x_29);
x_34 = 0;
x_15 = x_34;
x_16 = x_33;
goto block_28;
}
else
{
lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; uint8_t x_39;
x_35 = lean_ctor_get(x_29, 1);
lean_inc(x_35);
lean_dec(x_29);
x_36 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(x_14, x_7, x_8, x_9, x_10, x_11, x_12, x_35);
x_37 = lean_ctor_get(x_36, 0);
lean_inc(x_37);
x_38 = lean_ctor_get(x_37, 3);
x_38 = lean_ctor_get(x_36, 1);
lean_inc(x_38);
lean_dec(x_36);
x_39 = lean_unbox(x_37);
lean_dec(x_37);
x_39 = lean_ctor_get_uint8(x_38, sizeof(void*)*1);
lean_dec(x_38);
if (x_39 == 0)
{
lean_object* x_40; uint8_t x_41;
x_40 = lean_ctor_get(x_36, 1);
lean_inc(x_40);
lean_dec(x_36);
x_41 = 0;
x_22 = x_41;
x_23 = x_40;
goto block_35;
x_15 = x_39;
x_16 = x_38;
goto block_28;
}
else
block_28:
{
lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; uint8_t x_46;
x_42 = lean_ctor_get(x_36, 1);
lean_inc(x_42);
lean_dec(x_36);
x_43 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__2(x_21, x_9, x_10, x_11, x_12, x_13, x_14, x_42);
x_44 = lean_ctor_get(x_43, 0);
lean_inc(x_44);
x_45 = lean_ctor_get(x_43, 1);
lean_inc(x_45);
lean_dec(x_43);
x_46 = lean_unbox(x_44);
lean_dec(x_44);
x_22 = x_46;
x_23 = x_45;
goto block_35;
}
block_35:
{
if (x_22 == 0)
{
lean_object* x_24; lean_object* x_25;
x_24 = lean_box(0);
x_25 = l_Lean_Elab_wfRecursion___lambda__1(x_1, x_7, x_19, x_5, x_17, x_6, x_24, x_9, x_10, x_11, x_12, x_13, x_14, x_23);
return x_25;
}
else
{
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_object* x_32; lean_object* x_33; lean_object* x_34;
lean_inc(x_19);
x_26 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_26, 0, x_19);
x_27 = l_Lean_Elab_wfRecursion___lambda__2___closed__2;
x_28 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_28, 0, x_27);
lean_ctor_set(x_28, 1, x_26);
x_29 = l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs___spec__1___closed__8;
x_30 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_30, 0, x_28);
lean_ctor_set(x_30, 1, x_29);
x_31 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_21, x_30, x_9, x_10, x_11, x_12, x_13, x_14, x_23);
x_32 = lean_ctor_get(x_31, 0);
lean_inc(x_32);
x_33 = lean_ctor_get(x_31, 1);
lean_inc(x_33);
lean_dec(x_31);
x_34 = l_Lean_Elab_wfRecursion___lambda__1(x_1, x_7, x_19, x_5, x_17, x_6, x_32, x_9, x_10, x_11, x_12, x_13, x_14, x_33);
lean_dec(x_32);
return x_34;
}
}
}
else
{
uint8_t x_47;
lean_dec(x_17);
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_1);
x_47 = !lean_is_exclusive(x_18);
if (x_47 == 0)
if (x_15 == 0)
{
lean_object* x_17; lean_object* x_18;
x_17 = lean_box(0);
x_18 = l_Lean_Elab_wfRecursion___lambda__1(x_1, x_2, x_6, x_3, x_4, x_5, x_17, x_7, x_8, x_9, x_10, x_11, x_12, x_16);
return x_18;
}
else
{
lean_object* x_48; lean_object* x_49; lean_object* x_50;
x_48 = lean_ctor_get(x_18, 0);
x_49 = lean_ctor_get(x_18, 1);
lean_inc(x_49);
lean_inc(x_48);
lean_dec(x_18);
x_50 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_50, 0, x_48);
lean_ctor_set(x_50, 1, x_49);
return x_50;
lean_object* x_19; lean_object* x_20; 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;
lean_inc(x_6);
x_19 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_19, 0, x_6);
x_20 = l_Lean_Elab_wfRecursion___lambda__2___closed__2;
x_21 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
x_22 = l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs___spec__1___closed__8;
x_23 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_23, 0, x_21);
lean_ctor_set(x_23, 1, x_22);
x_24 = l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(x_14, x_23, x_7, x_8, x_9, x_10, x_11, x_12, x_16);
x_25 = lean_ctor_get(x_24, 0);
lean_inc(x_25);
x_26 = lean_ctor_get(x_24, 1);
lean_inc(x_26);
lean_dec(x_24);
x_27 = l_Lean_Elab_wfRecursion___lambda__1(x_1, x_2, x_6, x_3, x_4, x_5, x_25, x_7, x_8, x_9, x_10, x_11, x_12, x_26);
lean_dec(x_25);
return x_27;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__3(size_t x_1, size_t 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* x_13) {
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__3(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* x_13, lean_object* x_14, lean_object* x_15) {
_start:
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_16 = l_Lean_Expr_bindingDomain_x21(x_8);
x_17 = lean_ctor_get(x_1, 3);
lean_inc(x_17);
lean_inc(x_17);
x_18 = lean_alloc_closure((void*)(l_Lean_Elab_wfRecursion___lambda__2), 13, 5);
lean_closure_set(x_18, 0, x_1);
lean_closure_set(x_18, 1, x_7);
lean_closure_set(x_18, 2, x_2);
lean_closure_set(x_18, 3, x_17);
lean_closure_set(x_18, 4, x_3);
x_19 = l_Lean_Elab_WF_elabWFRel___rarg(x_4, x_17, x_5, x_16, x_6, x_18, x_9, x_10, x_11, x_12, x_13, x_14, x_15);
return x_19;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__4(size_t x_1, size_t 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* x_13) {
_start:
{
lean_object* x_14;
@ -4445,14 +4411,13 @@ lean_inc(x_11);
x_14 = l_Array_mapMUnsafe_map___at_Lean_Elab_addAndCompileUnsafe___spec__1(x_1, x_2, x_3, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_15; lean_object* x_16; uint8_t x_17; uint8_t x_18; lean_object* x_19;
lean_object* x_15; lean_object* x_16; uint8_t x_17; lean_object* x_18;
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_ctor_get(x_14, 1);
lean_inc(x_16);
lean_dec(x_14);
x_17 = 0;
x_18 = 1;
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
@ -4460,13 +4425,13 @@ lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_4);
x_19 = l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux(x_4, x_17, x_18, x_7, x_8, x_9, x_10, x_11, x_12, x_16);
if (lean_obj_tag(x_19) == 0)
x_18 = l___private_Lean_Elab_PreDefinition_Basic_0__Lean_Elab_addNonRecAux(x_4, x_17, x_17, x_7, x_8, x_9, x_10, x_11, x_12, x_16);
if (lean_obj_tag(x_18) == 0)
{
lean_object* x_20; lean_object* x_21;
x_20 = lean_ctor_get(x_19, 1);
lean_inc(x_20);
lean_dec(x_19);
lean_object* x_19; lean_object* x_20;
x_19 = lean_ctor_get(x_18, 1);
lean_inc(x_19);
lean_dec(x_18);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
@ -4475,41 +4440,41 @@ lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_4);
lean_inc(x_15);
x_21 = l___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs(x_15, x_4, x_5, x_7, x_8, x_9, x_10, x_11, x_12, x_20);
if (lean_obj_tag(x_21) == 0)
x_20 = l___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_addNonRecPreDefs(x_15, x_4, x_5, x_7, x_8, x_9, x_10, x_11, x_12, x_19);
if (lean_obj_tag(x_20) == 0)
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; size_t x_27; lean_object* x_28; lean_object* x_29;
x_22 = lean_ctor_get(x_21, 1);
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; size_t x_26; lean_object* x_27; lean_object* x_28;
x_21 = lean_ctor_get(x_20, 1);
lean_inc(x_21);
lean_dec(x_20);
x_22 = lean_ctor_get(x_4, 3);
lean_inc(x_22);
lean_dec(x_21);
x_23 = lean_ctor_get(x_4, 3);
lean_inc(x_23);
lean_dec(x_4);
lean_inc(x_15);
x_24 = l_Lean_Elab_WF_registerEqnsInfo(x_15, x_23, x_11, x_12, x_22);
x_25 = lean_ctor_get(x_24, 1);
lean_inc(x_25);
lean_dec(x_24);
x_26 = lean_array_get_size(x_15);
x_27 = lean_usize_of_nat(x_26);
lean_dec(x_26);
x_28 = lean_box(0);
x_23 = l_Lean_Elab_WF_registerEqnsInfo(x_15, x_22, x_11, x_12, x_21);
x_24 = lean_ctor_get(x_23, 1);
lean_inc(x_24);
lean_dec(x_23);
x_25 = lean_array_get_size(x_15);
x_26 = lean_usize_of_nat(x_25);
lean_dec(x_25);
x_27 = lean_box(0);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_7);
x_29 = l_Array_forInUnsafe_loop___at_Lean_Elab_wfRecursion___spec__1(x_15, x_27, x_2, x_28, x_7, x_8, x_9, x_10, x_11, x_12, x_25);
if (lean_obj_tag(x_29) == 0)
x_28 = l_Array_forInUnsafe_loop___at_Lean_Elab_wfRecursion___spec__1(x_15, x_26, x_2, x_27, x_7, x_8, x_9, x_10, x_11, x_12, x_24);
if (lean_obj_tag(x_28) == 0)
{
lean_object* x_30; lean_object* x_31;
x_30 = lean_ctor_get(x_29, 1);
lean_inc(x_30);
lean_dec(x_29);
x_31 = l_Lean_Elab_addAndCompilePartialRec(x_15, x_7, x_8, x_9, x_10, x_11, x_12, x_30);
return x_31;
lean_object* x_29; lean_object* x_30;
x_29 = lean_ctor_get(x_28, 1);
lean_inc(x_29);
lean_dec(x_28);
x_30 = l_Lean_Elab_addAndCompilePartialRec(x_15, x_7, x_8, x_9, x_10, x_11, x_12, x_29);
return x_30;
}
else
{
uint8_t x_32;
uint8_t x_31;
lean_dec(x_15);
lean_dec(x_12);
lean_dec(x_11);
@ -4517,29 +4482,29 @@ lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
x_32 = !lean_is_exclusive(x_29);
if (x_32 == 0)
x_31 = !lean_is_exclusive(x_28);
if (x_31 == 0)
{
return x_29;
return x_28;
}
else
{
lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_33 = lean_ctor_get(x_29, 0);
x_34 = lean_ctor_get(x_29, 1);
lean_inc(x_34);
lean_object* x_32; lean_object* x_33; lean_object* x_34;
x_32 = lean_ctor_get(x_28, 0);
x_33 = lean_ctor_get(x_28, 1);
lean_inc(x_33);
lean_dec(x_29);
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_33);
lean_ctor_set(x_35, 1, x_34);
return x_35;
lean_inc(x_32);
lean_dec(x_28);
x_34 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_34, 0, x_32);
lean_ctor_set(x_34, 1, x_33);
return x_34;
}
}
}
else
{
uint8_t x_36;
uint8_t x_35;
lean_dec(x_15);
lean_dec(x_12);
lean_dec(x_11);
@ -4548,29 +4513,29 @@ lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_4);
x_36 = !lean_is_exclusive(x_21);
if (x_36 == 0)
x_35 = !lean_is_exclusive(x_20);
if (x_35 == 0)
{
return x_21;
return x_20;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_37 = lean_ctor_get(x_21, 0);
x_38 = lean_ctor_get(x_21, 1);
lean_inc(x_38);
lean_object* x_36; lean_object* x_37; lean_object* x_38;
x_36 = lean_ctor_get(x_20, 0);
x_37 = lean_ctor_get(x_20, 1);
lean_inc(x_37);
lean_dec(x_21);
x_39 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_39, 0, x_37);
lean_ctor_set(x_39, 1, x_38);
return x_39;
lean_inc(x_36);
lean_dec(x_20);
x_38 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_38, 0, x_36);
lean_ctor_set(x_38, 1, x_37);
return x_38;
}
}
}
else
{
uint8_t x_40;
uint8_t x_39;
lean_dec(x_15);
lean_dec(x_12);
lean_dec(x_11);
@ -4580,29 +4545,29 @@ lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
x_40 = !lean_is_exclusive(x_19);
if (x_40 == 0)
x_39 = !lean_is_exclusive(x_18);
if (x_39 == 0)
{
return x_19;
return x_18;
}
else
{
lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_41 = lean_ctor_get(x_19, 0);
x_42 = lean_ctor_get(x_19, 1);
lean_inc(x_42);
lean_object* x_40; lean_object* x_41; lean_object* x_42;
x_40 = lean_ctor_get(x_18, 0);
x_41 = lean_ctor_get(x_18, 1);
lean_inc(x_41);
lean_dec(x_19);
x_43 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_43, 0, x_41);
lean_ctor_set(x_43, 1, x_42);
return x_43;
lean_inc(x_40);
lean_dec(x_18);
x_42 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_42, 0, x_40);
lean_ctor_set(x_42, 1, x_41);
return x_42;
}
}
}
else
{
uint8_t x_44;
uint8_t x_43;
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
@ -4611,28 +4576,28 @@ lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
x_44 = !lean_is_exclusive(x_14);
if (x_44 == 0)
x_43 = !lean_is_exclusive(x_14);
if (x_43 == 0)
{
return x_14;
}
else
{
lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_45 = lean_ctor_get(x_14, 0);
x_46 = lean_ctor_get(x_14, 1);
lean_inc(x_46);
lean_object* x_44; lean_object* x_45; lean_object* x_46;
x_44 = lean_ctor_get(x_14, 0);
x_45 = lean_ctor_get(x_14, 1);
lean_inc(x_45);
lean_inc(x_44);
lean_dec(x_14);
x_47 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_47, 0, x_45);
lean_ctor_set(x_47, 1, x_46);
return x_47;
x_46 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_46, 0, x_44);
lean_ctor_set(x_46, 1, x_45);
return x_46;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__4(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_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11;
@ -4877,7 +4842,7 @@ lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_1);
x_76 = l_Lean_Elab_wfRecursion___lambda__4(x_71, x_1, x_67, x_4, x_5, x_6, x_7, x_8, x_9, x_75);
x_76 = l_Lean_Elab_wfRecursion___lambda__5(x_71, x_1, x_67, x_4, x_5, x_6, x_7, x_8, x_9, x_75);
if (lean_obj_tag(x_76) == 0)
{
lean_object* x_77; lean_object* x_78;
@ -4959,7 +4924,7 @@ lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_1);
x_96 = l_Lean_Elab_wfRecursion___lambda__4(x_71, x_1, x_94, x_4, x_5, x_6, x_7, x_8, x_9, x_95);
x_96 = l_Lean_Elab_wfRecursion___lambda__5(x_71, x_1, x_94, x_4, x_5, x_6, x_7, x_8, x_9, x_95);
lean_dec(x_94);
if (lean_obj_tag(x_96) == 0)
{
@ -5114,16 +5079,16 @@ lean_inc(x_24);
lean_inc(x_23);
x_25 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_25, 0, x_23);
lean_inc(x_24);
lean_inc(x_23);
lean_inc(x_1);
x_26 = lean_alloc_closure((void*)(l_Lean_Elab_wfRecursion___lambda__2), 15, 6);
lean_inc(x_24);
x_26 = lean_alloc_closure((void*)(l_Lean_Elab_wfRecursion___lambda__3___boxed), 15, 6);
lean_closure_set(x_26, 0, x_21);
lean_closure_set(x_26, 1, x_1);
lean_closure_set(x_26, 2, x_23);
lean_closure_set(x_26, 3, x_2);
lean_closure_set(x_26, 4, x_3);
lean_closure_set(x_26, 5, x_24);
lean_closure_set(x_26, 1, x_3);
lean_closure_set(x_26, 2, x_24);
lean_closure_set(x_26, 3, x_1);
lean_closure_set(x_26, 4, x_23);
lean_closure_set(x_26, 5, x_2);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
@ -5183,7 +5148,7 @@ if (x_31 == 0)
{
lean_object* x_33; lean_object* x_34;
x_33 = lean_box(0);
x_34 = l_Lean_Elab_wfRecursion___lambda__3(x_12, x_13, x_1, x_28, x_23, x_33, x_4, x_5, x_6, x_7, x_8, x_9, x_32);
x_34 = l_Lean_Elab_wfRecursion___lambda__4(x_12, x_13, x_1, x_28, x_23, x_33, x_4, x_5, x_6, x_7, x_8, x_9, x_32);
return x_34;
}
else
@ -5218,7 +5183,7 @@ lean_inc(x_47);
x_48 = lean_ctor_get(x_46, 1);
lean_inc(x_48);
lean_dec(x_46);
x_49 = l_Lean_Elab_wfRecursion___lambda__3(x_12, x_13, x_1, x_28, x_23, x_47, x_4, x_5, x_6, x_7, x_8, x_9, x_48);
x_49 = l_Lean_Elab_wfRecursion___lambda__4(x_12, x_13, x_1, x_28, x_23, x_47, x_4, x_5, x_6, x_7, x_8, x_9, x_48);
lean_dec(x_47);
return x_49;
}
@ -5300,7 +5265,16 @@ lean_dec(x_7);
return x_15;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__3___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, lean_object* x_13) {
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__3___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, lean_object* x_13, lean_object* x_14, lean_object* x_15) {
_start:
{
lean_object* x_16;
x_16 = l_Lean_Elab_wfRecursion___lambda__3(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15);
lean_dec(x_8);
return x_16;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__4___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, lean_object* x_13) {
_start:
{
size_t x_14; size_t x_15; lean_object* x_16;
@ -5308,23 +5282,23 @@ x_14 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_15 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_16 = l_Lean_Elab_wfRecursion___lambda__3(x_14, x_15, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
x_16 = l_Lean_Elab_wfRecursion___lambda__4(x_14, x_15, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
lean_dec(x_6);
return x_16;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__4___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_EXPORT lean_object* l_Lean_Elab_wfRecursion___lambda__5___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) {
_start:
{
lean_object* x_11;
x_11 = l_Lean_Elab_wfRecursion___lambda__4(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_11 = l_Lean_Elab_wfRecursion___lambda__5(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
return x_11;
}
}
LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_PreDefinition_WF_Main___hyg_2032_(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_PreDefinition_WF_Main___hyg_2027_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -5458,7 +5432,7 @@ l_Lean_Elab_wfRecursion___closed__5 = _init_l_Lean_Elab_wfRecursion___closed__5(
lean_mark_persistent(l_Lean_Elab_wfRecursion___closed__5);
l_Lean_Elab_wfRecursion___closed__6 = _init_l_Lean_Elab_wfRecursion___closed__6();
lean_mark_persistent(l_Lean_Elab_wfRecursion___closed__6);
res = l_Lean_Elab_initFn____x40_Lean_Elab_PreDefinition_WF_Main___hyg_2032_(lean_io_mk_world());
res = l_Lean_Elab_initFn____x40_Lean_Elab_PreDefinition_WF_Main___hyg_2027_(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));

5436
stage0/stdlib/Lean/Elab/PreDefinition/WF/Rel.c generated
View file

File diff suppressed because it is too large Load diff

724
stage0/stdlib/Lean/Meta/Tactic/LinearArith/Basic.c generated Normal file
View file

@ -0,0 +1,724 @@
// Lean compiler output
// Module: Lean.Meta.Tactic.LinearArith.Basic
// Imports: Init Lean.Expr
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
LEAN_EXPORT lean_object* l_Lean_Meta_Linear_isLinearTerm___boxed(lean_object*);
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__19;
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__13;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Linear_isLinearCnstr___boxed(lean_object*);
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__4;
uint8_t lean_name_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__12;
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__8;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__21;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__2;
lean_object* l_Lean_Expr_appArg_x21(lean_object*);
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__14;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__13;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__1;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__4;
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__9;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__17;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__9;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__8;
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__12;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__15;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__22;
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__1;
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__2;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__3;
uint8_t l_Lean_Expr_isConst(lean_object*);
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__14;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__5;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__18;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__6;
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__7;
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__16;
lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__10;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__20;
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__11;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__5;
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__3;
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__15;
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__7;
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__6;
lean_object* l_Lean_Expr_getAppFn(lean_object*);
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__16;
LEAN_EXPORT uint8_t l_Lean_Meta_Linear_isLinearTerm(lean_object*);
LEAN_EXPORT uint8_t l_Lean_Meta_Linear_isLinearCnstr(lean_object*);
lean_object* l_Lean_Expr_constName_x21(lean_object*);
static lean_object* l_Lean_Meta_Linear_isLinearCnstr___closed__11;
static lean_object* l_Lean_Meta_Linear_isLinearTerm___closed__10;
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("HAdd");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___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_Linear_isLinearTerm___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("hAdd");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Linear_isLinearTerm___closed__2;
x_2 = l_Lean_Meta_Linear_isLinearTerm___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("HMul");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Linear_isLinearTerm___closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("hMul");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Linear_isLinearTerm___closed__6;
x_2 = l_Lean_Meta_Linear_isLinearTerm___closed__7;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___closed__9() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("HSub");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Linear_isLinearTerm___closed__9;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___closed__11() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("hSub");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Linear_isLinearTerm___closed__10;
x_2 = l_Lean_Meta_Linear_isLinearTerm___closed__11;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___closed__13() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Nat");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Linear_isLinearTerm___closed__13;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___closed__15() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("succ");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearTerm___closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Linear_isLinearTerm___closed__14;
x_2 = l_Lean_Meta_Linear_isLinearTerm___closed__15;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT uint8_t l_Lean_Meta_Linear_isLinearTerm(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3;
x_2 = l_Lean_Expr_getAppFn(x_1);
x_3 = l_Lean_Expr_isConst(x_2);
if (x_3 == 0)
{
uint8_t x_4;
lean_dec(x_2);
x_4 = 0;
return x_4;
}
else
{
lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_5 = l_Lean_Expr_constName_x21(x_2);
lean_dec(x_2);
x_6 = l_Lean_Meta_Linear_isLinearTerm___closed__4;
x_7 = lean_name_eq(x_5, x_6);
if (x_7 == 0)
{
lean_object* x_8; uint8_t x_9;
x_8 = l_Lean_Meta_Linear_isLinearTerm___closed__8;
x_9 = lean_name_eq(x_5, x_8);
if (x_9 == 0)
{
lean_object* x_10; uint8_t x_11;
x_10 = l_Lean_Meta_Linear_isLinearTerm___closed__12;
x_11 = lean_name_eq(x_5, x_10);
if (x_11 == 0)
{
lean_object* x_12; uint8_t x_13;
x_12 = l_Lean_Meta_Linear_isLinearTerm___closed__16;
x_13 = lean_name_eq(x_5, x_12);
lean_dec(x_5);
return x_13;
}
else
{
uint8_t x_14;
lean_dec(x_5);
x_14 = 1;
return x_14;
}
}
else
{
uint8_t x_15;
lean_dec(x_5);
x_15 = 1;
return x_15;
}
}
else
{
uint8_t x_16;
lean_dec(x_5);
x_16 = 1;
return x_16;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Linear_isLinearTerm___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Meta_Linear_isLinearTerm(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Eq");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___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_Linear_isLinearCnstr___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("LT");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Linear_isLinearCnstr___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lt");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Linear_isLinearCnstr___closed__4;
x_2 = l_Lean_Meta_Linear_isLinearCnstr___closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("LE");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Linear_isLinearCnstr___closed__7;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__9() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("le");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Linear_isLinearCnstr___closed__8;
x_2 = l_Lean_Meta_Linear_isLinearCnstr___closed__9;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__11() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("GT");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Linear_isLinearCnstr___closed__11;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__13() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("gt");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Linear_isLinearCnstr___closed__12;
x_2 = l_Lean_Meta_Linear_isLinearCnstr___closed__13;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__15() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("GE");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Linear_isLinearCnstr___closed__15;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__17() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("ge");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Linear_isLinearCnstr___closed__16;
x_2 = l_Lean_Meta_Linear_isLinearCnstr___closed__17;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__19() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Ne");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__20() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Linear_isLinearCnstr___closed__19;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__21() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Not");
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_Linear_isLinearCnstr___closed__22() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Linear_isLinearCnstr___closed__21;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT uint8_t l_Lean_Meta_Linear_isLinearCnstr(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3;
x_2 = l_Lean_Expr_getAppFn(x_1);
x_3 = l_Lean_Expr_isConst(x_2);
if (x_3 == 0)
{
uint8_t x_4;
lean_dec(x_2);
lean_dec(x_1);
x_4 = 0;
return x_4;
}
else
{
lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_5 = l_Lean_Expr_constName_x21(x_2);
lean_dec(x_2);
x_6 = l_Lean_Meta_Linear_isLinearCnstr___closed__2;
x_7 = lean_name_eq(x_5, x_6);
if (x_7 == 0)
{
lean_object* x_8; uint8_t x_9;
x_8 = l_Lean_Meta_Linear_isLinearCnstr___closed__6;
x_9 = lean_name_eq(x_5, x_8);
if (x_9 == 0)
{
lean_object* x_10; uint8_t x_11;
x_10 = l_Lean_Meta_Linear_isLinearCnstr___closed__10;
x_11 = lean_name_eq(x_5, x_10);
if (x_11 == 0)
{
lean_object* x_12; uint8_t x_13;
x_12 = l_Lean_Meta_Linear_isLinearCnstr___closed__14;
x_13 = lean_name_eq(x_5, x_12);
if (x_13 == 0)
{
lean_object* x_14; uint8_t x_15;
x_14 = l_Lean_Meta_Linear_isLinearCnstr___closed__18;
x_15 = lean_name_eq(x_5, x_14);
if (x_15 == 0)
{
lean_object* x_16; uint8_t x_17;
x_16 = l_Lean_Meta_Linear_isLinearCnstr___closed__20;
x_17 = lean_name_eq(x_5, x_16);
if (x_17 == 0)
{
lean_object* x_18; uint8_t x_19;
x_18 = l_Lean_Meta_Linear_isLinearCnstr___closed__22;
x_19 = lean_name_eq(x_5, x_18);
lean_dec(x_5);
if (x_19 == 0)
{
uint8_t x_20;
lean_dec(x_1);
x_20 = 0;
return x_20;
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_21 = lean_unsigned_to_nat(0u);
x_22 = l_Lean_Expr_getAppNumArgsAux(x_1, x_21);
x_23 = lean_unsigned_to_nat(1u);
x_24 = lean_nat_dec_eq(x_22, x_23);
lean_dec(x_22);
if (x_24 == 0)
{
uint8_t x_25;
lean_dec(x_1);
x_25 = 0;
return x_25;
}
else
{
lean_object* x_26;
x_26 = l_Lean_Expr_appArg_x21(x_1);
lean_dec(x_1);
x_1 = x_26;
goto _start;
}
}
}
else
{
uint8_t x_28;
lean_dec(x_5);
lean_dec(x_1);
x_28 = 1;
return x_28;
}
}
else
{
uint8_t x_29;
lean_dec(x_5);
lean_dec(x_1);
x_29 = 1;
return x_29;
}
}
else
{
uint8_t x_30;
lean_dec(x_5);
lean_dec(x_1);
x_30 = 1;
return x_30;
}
}
else
{
uint8_t x_31;
lean_dec(x_5);
lean_dec(x_1);
x_31 = 1;
return x_31;
}
}
else
{
uint8_t x_32;
lean_dec(x_5);
lean_dec(x_1);
x_32 = 1;
return x_32;
}
}
else
{
uint8_t x_33;
lean_dec(x_5);
lean_dec(x_1);
x_33 = 1;
return x_33;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_Linear_isLinearCnstr___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Meta_Linear_isLinearCnstr(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
lean_object* initialize_Init(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Expr(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Meta_Tactic_LinearArith_Basic(uint8_t builtin, lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Expr(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Meta_Linear_isLinearTerm___closed__1 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__1();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__1);
l_Lean_Meta_Linear_isLinearTerm___closed__2 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__2();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__2);
l_Lean_Meta_Linear_isLinearTerm___closed__3 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__3();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__3);
l_Lean_Meta_Linear_isLinearTerm___closed__4 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__4();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__4);
l_Lean_Meta_Linear_isLinearTerm___closed__5 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__5();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__5);
l_Lean_Meta_Linear_isLinearTerm___closed__6 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__6();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__6);
l_Lean_Meta_Linear_isLinearTerm___closed__7 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__7();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__7);
l_Lean_Meta_Linear_isLinearTerm___closed__8 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__8();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__8);
l_Lean_Meta_Linear_isLinearTerm___closed__9 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__9();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__9);
l_Lean_Meta_Linear_isLinearTerm___closed__10 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__10();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__10);
l_Lean_Meta_Linear_isLinearTerm___closed__11 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__11();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__11);
l_Lean_Meta_Linear_isLinearTerm___closed__12 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__12();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__12);
l_Lean_Meta_Linear_isLinearTerm___closed__13 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__13();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__13);
l_Lean_Meta_Linear_isLinearTerm___closed__14 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__14();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__14);
l_Lean_Meta_Linear_isLinearTerm___closed__15 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__15();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__15);
l_Lean_Meta_Linear_isLinearTerm___closed__16 = _init_l_Lean_Meta_Linear_isLinearTerm___closed__16();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearTerm___closed__16);
l_Lean_Meta_Linear_isLinearCnstr___closed__1 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__1();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__1);
l_Lean_Meta_Linear_isLinearCnstr___closed__2 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__2();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__2);
l_Lean_Meta_Linear_isLinearCnstr___closed__3 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__3();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__3);
l_Lean_Meta_Linear_isLinearCnstr___closed__4 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__4();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__4);
l_Lean_Meta_Linear_isLinearCnstr___closed__5 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__5();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__5);
l_Lean_Meta_Linear_isLinearCnstr___closed__6 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__6();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__6);
l_Lean_Meta_Linear_isLinearCnstr___closed__7 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__7();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__7);
l_Lean_Meta_Linear_isLinearCnstr___closed__8 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__8();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__8);
l_Lean_Meta_Linear_isLinearCnstr___closed__9 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__9();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__9);
l_Lean_Meta_Linear_isLinearCnstr___closed__10 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__10();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__10);
l_Lean_Meta_Linear_isLinearCnstr___closed__11 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__11();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__11);
l_Lean_Meta_Linear_isLinearCnstr___closed__12 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__12();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__12);
l_Lean_Meta_Linear_isLinearCnstr___closed__13 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__13();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__13);
l_Lean_Meta_Linear_isLinearCnstr___closed__14 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__14();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__14);
l_Lean_Meta_Linear_isLinearCnstr___closed__15 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__15();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__15);
l_Lean_Meta_Linear_isLinearCnstr___closed__16 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__16();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__16);
l_Lean_Meta_Linear_isLinearCnstr___closed__17 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__17();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__17);
l_Lean_Meta_Linear_isLinearCnstr___closed__18 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__18();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__18);
l_Lean_Meta_Linear_isLinearCnstr___closed__19 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__19();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__19);
l_Lean_Meta_Linear_isLinearCnstr___closed__20 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__20();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__20);
l_Lean_Meta_Linear_isLinearCnstr___closed__21 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__21();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__21);
l_Lean_Meta_Linear_isLinearCnstr___closed__22 = _init_l_Lean_Meta_Linear_isLinearCnstr___closed__22();
lean_mark_persistent(l_Lean_Meta_Linear_isLinearCnstr___closed__22);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

7599
stage0/stdlib/Lean/Meta/Tactic/LinearArith/Nat.c generated
View file

File diff suppressed because it is too large Load diff

4556
stage0/stdlib/Lean/Meta/Tactic/LinearArith/Nat/Basic.c generated Normal file
View file

File diff suppressed because it is too large Load diff

3452
stage0/stdlib/Lean/Meta/Tactic/LinearArith/Nat/Simp.c generated Normal file
View file

File diff suppressed because it is too large Load diff

37
stage0/stdlib/Lean/Meta/Tactic/LinearArith/Nat/Solver.c generated Normal file
View file

@ -0,0 +1,37 @@
// Lean compiler output
// Module: Lean.Meta.Tactic.LinearArith.Nat.Solver
// Imports: Init Lean.Meta.Tactic.LinearArith.Solver Lean.Meta.Tactic.LinearArith.Nat.Basic
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* initialize_Init(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_LinearArith_Solver(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_LinearArith_Nat_Basic(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Meta_Tactic_LinearArith_Nat_Solver(uint8_t builtin, lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_LinearArith_Solver(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_LinearArith_Nat_Basic(builtin, 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));
}
#ifdef __cplusplus
}
#endif

672
stage0/stdlib/Lean/Meta/Tactic/LinearArith/Simp.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Meta.Tactic.LinearArith.Simp
// Imports: Init Lean.Meta.Tactic.LinearArith.Nat
// Imports: Init Lean.Meta.Tactic.LinearArith.Basic Lean.Meta.Tactic.LinearArith.Nat.Simp
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -13,608 +13,30 @@
#ifdef __cplusplus
extern "C" {
#endif
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__11;
lean_object* l_Lean_stringToMessageData(lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__12;
static lean_object* l_Lean_Meta_Linear_simp_x3f___closed__5;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Linear_simp_x3f___closed__3;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__17;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__8;
static lean_object* l_Lean_Meta_Linear_simp_x3f___closed__6;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__11;
lean_object* lean_st_ref_get(lean_object*, lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__20;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__9;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__8;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___boxed(lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__1;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__4;
lean_object* l_Lean_Expr_appArg_x21(lean_object*);
static lean_object* l_Lean_Meta_Linear_simp_x3f___closed__1;
static lean_object* l_Lean_Meta_Linear_simp_x3f___closed__10;
lean_object* l_Lean_Meta_Linear_Nat_simpExpr_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__2;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__4;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__9;
lean_object* l_Lean_Meta_Linear_Nat_simpCnstr_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__10;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__13;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__1;
static lean_object* l_Lean_Meta_Linear_simp_x3f___closed__7;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___boxed(lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__15;
lean_object* l_Lean_addTrace___at_Lean_Meta_processPostponed_loop___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__3;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__12;
LEAN_EXPORT lean_object* l_Lean_Meta_Linear_simp_x3f___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__14;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__5;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__18;
LEAN_EXPORT uint8_t l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget(lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__5;
uint8_t l_Lean_Expr_isConst(lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__16;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_parentIsTarget___boxed(lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__14;
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___spec__14(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__13;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__6;
LEAN_EXPORT uint8_t l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Linear_simp_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__2;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__7;
static lean_object* l_Lean_Meta_Linear_simp_x3f___closed__2;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__16;
LEAN_EXPORT lean_object* l_Lean_Meta_Linear_simp_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_parentIsTarget(lean_object*);
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__10;
lean_object* l_Lean_Expr_getAppFn(lean_object*);
static lean_object* l_Lean_Meta_Linear_simp_x3f___closed__4;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__7;
uint8_t l_Lean_Meta_Linear_isLinearTerm(lean_object*);
static lean_object* l_Lean_Meta_Linear_simp_x3f___closed__9;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__3;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__15;
lean_object* l_Lean_Expr_constName_x21(lean_object*);
uint8_t l_Lean_Meta_Linear_isLinearCnstr(lean_object*);
static lean_object* l_Lean_Meta_Linear_simp_x3f___closed__8;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__19;
static lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__6;
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("HAdd");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("hAdd");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__2;
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("HMul");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("hMul");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__6;
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__7;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__9() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("HSub");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__9;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__11() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("hSub");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__10;
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__11;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__13() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Nat");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__13;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__15() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("succ");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__14;
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__15;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT uint8_t l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3;
x_2 = l_Lean_Expr_getAppFn(x_1);
x_3 = l_Lean_Expr_isConst(x_2);
if (x_3 == 0)
{
uint8_t x_4;
lean_dec(x_2);
x_4 = 0;
return x_4;
}
else
{
lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_5 = l_Lean_Expr_constName_x21(x_2);
lean_dec(x_2);
x_6 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__4;
x_7 = lean_name_eq(x_5, x_6);
if (x_7 == 0)
{
lean_object* x_8; uint8_t x_9;
x_8 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__8;
x_9 = lean_name_eq(x_5, x_8);
if (x_9 == 0)
{
lean_object* x_10; uint8_t x_11;
x_10 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__12;
x_11 = lean_name_eq(x_5, x_10);
if (x_11 == 0)
{
lean_object* x_12; uint8_t x_13;
x_12 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__16;
x_13 = lean_name_eq(x_5, x_12);
lean_dec(x_5);
return x_13;
}
else
{
uint8_t x_14;
lean_dec(x_5);
x_14 = 1;
return x_14;
}
}
else
{
uint8_t x_15;
lean_dec(x_5);
x_15 = 1;
return x_15;
}
}
else
{
uint8_t x_16;
lean_dec(x_5);
x_16 = 1;
return x_16;
}
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Eq");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("LT");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lt");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__4;
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__5;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("LE");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__7;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__9() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("le");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__8;
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__9;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__11() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("GT");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__11;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__13() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("gt");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__14() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__12;
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__13;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__15() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("GE");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__16() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__15;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__17() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("ge");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__18() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__16;
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__17;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__19() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Not");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__20() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__19;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT uint8_t l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3;
x_2 = l_Lean_Expr_getAppFn(x_1);
x_3 = l_Lean_Expr_isConst(x_2);
if (x_3 == 0)
{
uint8_t x_4;
lean_dec(x_2);
lean_dec(x_1);
x_4 = 0;
return x_4;
}
else
{
lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_5 = l_Lean_Expr_constName_x21(x_2);
lean_dec(x_2);
x_6 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__2;
x_7 = lean_name_eq(x_5, x_6);
if (x_7 == 0)
{
lean_object* x_8; uint8_t x_9;
x_8 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__6;
x_9 = lean_name_eq(x_5, x_8);
if (x_9 == 0)
{
lean_object* x_10; uint8_t x_11;
x_10 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__10;
x_11 = lean_name_eq(x_5, x_10);
if (x_11 == 0)
{
lean_object* x_12; uint8_t x_13;
x_12 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__14;
x_13 = lean_name_eq(x_5, x_12);
if (x_13 == 0)
{
lean_object* x_14; uint8_t x_15;
x_14 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__18;
x_15 = lean_name_eq(x_5, x_14);
if (x_15 == 0)
{
lean_object* x_16; uint8_t x_17;
x_16 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__20;
x_17 = lean_name_eq(x_5, x_16);
lean_dec(x_5);
if (x_17 == 0)
{
uint8_t x_18;
lean_dec(x_1);
x_18 = 0;
return x_18;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22;
x_19 = lean_unsigned_to_nat(0u);
x_20 = l_Lean_Expr_getAppNumArgsAux(x_1, x_19);
x_21 = lean_unsigned_to_nat(1u);
x_22 = lean_nat_dec_eq(x_20, x_21);
lean_dec(x_20);
if (x_22 == 0)
{
uint8_t x_23;
lean_dec(x_1);
x_23 = 0;
return x_23;
}
else
{
lean_object* x_24;
x_24 = l_Lean_Expr_appArg_x21(x_1);
lean_dec(x_1);
x_1 = x_24;
goto _start;
}
}
}
else
{
uint8_t x_26;
lean_dec(x_5);
lean_dec(x_1);
x_26 = 1;
return x_26;
}
}
else
{
uint8_t x_27;
lean_dec(x_5);
lean_dec(x_1);
x_27 = 1;
return x_27;
}
}
else
{
uint8_t x_28;
lean_dec(x_5);
lean_dec(x_1);
x_28 = 1;
return x_28;
}
}
else
{
uint8_t x_29;
lean_dec(x_5);
lean_dec(x_1);
x_29 = 1;
return x_29;
}
}
else
{
uint8_t x_30;
lean_dec(x_5);
lean_dec(x_1);
x_30 = 1;
return x_30;
}
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
LEAN_EXPORT uint8_t l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_parentIsTarget(lean_object* x_1) {
_start:
{
@ -630,11 +52,11 @@ lean_object* x_3; uint8_t x_4;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
lean_dec(x_1);
x_4 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget(x_3);
x_4 = l_Lean_Meta_Linear_isLinearTerm(x_3);
if (x_4 == 0)
{
uint8_t x_5;
x_5 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget(x_3);
x_5 = l_Lean_Meta_Linear_isLinearCnstr(x_3);
return x_5;
}
else
@ -757,11 +179,11 @@ _start:
{
uint8_t x_8;
lean_inc(x_1);
x_8 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget(x_1);
x_8 = l_Lean_Meta_Linear_isLinearCnstr(x_1);
if (x_8 == 0)
{
uint8_t x_9;
x_9 = l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget(x_1);
x_9 = l_Lean_Meta_Linear_isLinearTerm(x_1);
if (x_9 == 0)
{
lean_object* x_10; lean_object* x_11;
@ -888,7 +310,8 @@ return x_8;
}
}
lean_object* initialize_Init(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_LinearArith_Nat(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_LinearArith_Basic(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Meta_Tactic_LinearArith_Nat_Simp(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Lean_Meta_Tactic_LinearArith_Simp(uint8_t builtin, lean_object* w) {
lean_object * res;
@ -897,81 +320,12 @@ _G_initialized = true;
res = initialize_Init(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_LinearArith_Nat(builtin, lean_io_mk_world());
res = initialize_Lean_Meta_Tactic_LinearArith_Basic(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_LinearArith_Nat_Simp(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__1 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__1();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__1);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__2 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__2();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__2);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__3 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__3();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__3);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__4 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__4();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__4);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__5 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__5();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__5);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__6 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__6();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__6);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__7 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__7();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__7);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__8 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__8();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__8);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__9 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__9();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__9);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__10 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__10();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__10);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__11 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__11();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__11);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__12 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__12();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__12);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__13 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__13();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__13);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__14 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__14();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__14);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__15 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__15();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__15);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__16 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__16();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpExprTarget___closed__16);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__1 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__1();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__1);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__2 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__2();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__2);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__3 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__3();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__3);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__4 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__4();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__4);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__5 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__5();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__5);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__6 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__6();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__6);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__7 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__7();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__7);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__8 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__8();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__8);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__9 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__9();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__9);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__10 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__10();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__10);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__11 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__11();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__11);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__12 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__12();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__12);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__13 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__13();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__13);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__14 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__14();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__14);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__15 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__15();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__15);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__16 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__16();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__16);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__17 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__17();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__17);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__18 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__18();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__18);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__19 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__19();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__19);
l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__20 = _init_l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__20();
lean_mark_persistent(l___private_Lean_Meta_Tactic_LinearArith_Simp_0__Lean_Meta_Linear_isSimpCnstrTarget___closed__20);
l_Lean_Meta_Linear_simp_x3f___closed__1 = _init_l_Lean_Meta_Linear_simp_x3f___closed__1();
lean_mark_persistent(l_Lean_Meta_Linear_simp_x3f___closed__1);
l_Lean_Meta_Linear_simp_x3f___closed__2 = _init_l_Lean_Meta_Linear_simp_x3f___closed__2();

281
stage0/stdlib/Lean/Parser/Basic.c generated
View file

@ -131,7 +131,6 @@ LEAN_EXPORT lean_object* l_Lean_Parser_strLitFnAux(lean_object*, lean_object*, l
LEAN_EXPORT lean_object* l_Lean_Parser_minPrec;
LEAN_EXPORT lean_object* l_Lean_Parser_ParserState_next(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_setExpected___elambda__1___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_categoryParserFnRef;
LEAN_EXPORT lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_sepByFnAux_parse___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_Error_expected___default;
@ -243,7 +242,6 @@ LEAN_EXPORT lean_object* l_Lean_Parser_checkColGeFn___boxed(lean_object*, lean_o
static lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_reprLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_8641____closed__4;
static lean_object* l_Lean_Parser_instInhabitedParserInfo___closed__3;
LEAN_EXPORT lean_object* l_Lean_Parser_nameLitFn(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_setExpected___elambda__1___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_instInhabitedParserInfo___lambda__2___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_strLitFnAux___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_nameLitKind;
@ -288,7 +286,6 @@ LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insert___at_Lean_Parser_SyntaxN
static lean_object* l_Lean_Parser_whitespace___closed__1;
static lean_object* l_Lean_Parser_scientificLitNoAntiquot___closed__3;
LEAN_EXPORT lean_object* l_Lean_Parser_indexed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_setExpectedFn___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_mkAntiquotSplice___closed__9;
size_t lean_uint64_to_usize(uint64_t);
static lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_reprLeadingIdentBehavior____x40_Lean_Parser_Basic___hyg_8641____closed__13;
@ -319,7 +316,6 @@ static lean_object* l_Lean_Parser_termParser___closed__1;
LEAN_EXPORT lean_object* l_Lean_Parser_mkIdResult___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_fieldIdx___closed__1;
LEAN_EXPORT lean_object* l_Lean_Parser_TokenMap_insert(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_setExpected___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_unicodeSymbol(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_longestMatchFn___closed__1;
LEAN_EXPORT lean_object* l_Lean_Parser_checkStackTopFn(lean_object*, lean_object*, lean_object*, lean_object*);
@ -472,7 +468,7 @@ static lean_object* l_Lean_Parser_dbgTraceStateFn___closed__7;
LEAN_EXPORT lean_object* l_Lean_Parser_longestMatchStep(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_instAndThenParser(lean_object*, lean_object*);
uint8_t l_Lean_Name_quickCmp(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_setExpectedFn(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_setExpectedFn(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_strLitFn(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_mkAntiquot___closed__12;
LEAN_EXPORT lean_object* l_Lean_Parser_ParserContext_savedPos_x3f___default;
@ -765,7 +761,6 @@ static lean_object* l_Lean_Parser_FirstTokens_toStr___closed__1;
LEAN_EXPORT lean_object* l_Lean_Parser_dbgTraceStateFn___lambda__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_withoutInfo___elambda__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_sepByFnAux(lean_object*, lean_object*, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_setExpectedFn___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_ParserModuleContext_openDecls___default;
LEAN_EXPORT lean_object* l_Lean_Parser_withResultOf(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__6___rarg___boxed(lean_object*, lean_object*);
@ -963,7 +958,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_checkWsBefore___elambda__1___boxed(lean_o
LEAN_EXPORT lean_object* l_Lean_Parser_sepBy1___elambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_sepByFnAux_parse___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_TokenCacheEntry_stopPos___default;
LEAN_EXPORT lean_object* l_Lean_Parser_setExpected___elambda__1(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_setExpected___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_unicodeSymbolInfo___closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Parser_Basic_0__Lean_Parser_tokenFnAux(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Parser_hexNumberFn___lambda__1___boxed(lean_object*);
@ -26793,187 +26788,159 @@ lean_dec(x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_setExpectedFn___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
LEAN_EXPORT lean_object* l_Lean_Parser_setExpectedFn(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_apply_2(x_1, x_2, x_3);
x_5 = lean_ctor_get(x_4, 4);
lean_inc(x_5);
if (lean_obj_tag(x_5) == 0)
lean_object* x_5; lean_object* x_6;
x_5 = lean_apply_2(x_2, x_3, x_4);
x_6 = lean_ctor_get(x_5, 4);
lean_inc(x_6);
if (lean_obj_tag(x_6) == 0)
{
return x_4;
lean_dec(x_1);
return x_5;
}
else
{
uint8_t x_6;
x_6 = !lean_is_exclusive(x_5);
if (x_6 == 0)
{
uint8_t x_7;
x_7 = !lean_is_exclusive(x_4);
x_7 = !lean_is_exclusive(x_6);
if (x_7 == 0)
{
lean_object* x_8; lean_object* x_9; uint8_t x_10;
x_8 = lean_ctor_get(x_5, 0);
x_9 = lean_ctor_get(x_4, 4);
lean_dec(x_9);
x_10 = !lean_is_exclusive(x_8);
if (x_10 == 0)
uint8_t x_8;
x_8 = !lean_is_exclusive(x_5);
if (x_8 == 0)
{
lean_object* x_11; lean_object* x_12;
x_11 = lean_ctor_get(x_8, 1);
lean_dec(x_11);
x_12 = lean_box(0);
lean_ctor_set(x_8, 1, x_12);
return x_4;
lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_9 = lean_ctor_get(x_6, 0);
x_10 = lean_ctor_get(x_5, 4);
lean_dec(x_10);
x_11 = !lean_is_exclusive(x_9);
if (x_11 == 0)
{
lean_object* x_12;
x_12 = lean_ctor_get(x_9, 1);
lean_dec(x_12);
lean_ctor_set(x_9, 1, x_1);
return x_5;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_13 = lean_ctor_get(x_8, 0);
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_9, 0);
lean_inc(x_13);
lean_dec(x_8);
x_14 = lean_box(0);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_13);
lean_ctor_set(x_15, 1, x_14);
lean_ctor_set(x_5, 0, x_15);
return x_4;
lean_dec(x_9);
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_1);
lean_ctor_set(x_6, 0, x_14);
return x_5;
}
}
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_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
lean_object* x_15; 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_object* x_22; lean_object* x_23;
x_15 = lean_ctor_get(x_6, 0);
x_16 = lean_ctor_get(x_5, 0);
x_17 = lean_ctor_get(x_4, 0);
x_18 = lean_ctor_get(x_4, 1);
x_19 = lean_ctor_get(x_4, 2);
x_20 = lean_ctor_get(x_4, 3);
lean_inc(x_20);
x_17 = lean_ctor_get(x_5, 1);
x_18 = lean_ctor_get(x_5, 2);
x_19 = lean_ctor_get(x_5, 3);
lean_inc(x_19);
lean_inc(x_18);
lean_inc(x_17);
lean_dec(x_4);
x_21 = lean_ctor_get(x_16, 0);
lean_inc(x_21);
if (lean_is_exclusive(x_16)) {
lean_ctor_release(x_16, 0);
lean_ctor_release(x_16, 1);
x_22 = x_16;
lean_inc(x_16);
lean_dec(x_5);
x_20 = lean_ctor_get(x_15, 0);
lean_inc(x_20);
if (lean_is_exclusive(x_15)) {
lean_ctor_release(x_15, 0);
lean_ctor_release(x_15, 1);
x_21 = x_15;
} else {
lean_dec_ref(x_16);
x_22 = lean_box(0);
lean_dec_ref(x_15);
x_21 = lean_box(0);
}
x_23 = lean_box(0);
if (lean_is_scalar(x_22)) {
x_24 = lean_alloc_ctor(0, 2, 0);
if (lean_is_scalar(x_21)) {
x_22 = lean_alloc_ctor(0, 2, 0);
} else {
x_24 = x_22;
x_22 = x_21;
}
lean_ctor_set(x_24, 0, x_21);
lean_ctor_set(x_24, 1, x_23);
lean_ctor_set(x_5, 0, x_24);
x_25 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_25, 0, x_17);
lean_ctor_set(x_25, 1, x_18);
lean_ctor_set(x_25, 2, x_19);
lean_ctor_set(x_25, 3, x_20);
lean_ctor_set(x_25, 4, x_5);
return x_25;
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_1);
lean_ctor_set(x_6, 0, x_22);
x_23 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_23, 0, x_16);
lean_ctor_set(x_23, 1, x_17);
lean_ctor_set(x_23, 2, x_18);
lean_ctor_set(x_23, 3, x_19);
lean_ctor_set(x_23, 4, x_6);
return x_23;
}
}
else
{
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_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37;
x_26 = lean_ctor_get(x_5, 0);
lean_object* x_24; lean_object* x_25; 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_object* x_32; lean_object* x_33; lean_object* x_34;
x_24 = lean_ctor_get(x_6, 0);
lean_inc(x_24);
lean_dec(x_6);
x_25 = lean_ctor_get(x_5, 0);
lean_inc(x_25);
x_26 = lean_ctor_get(x_5, 1);
lean_inc(x_26);
lean_dec(x_5);
x_27 = lean_ctor_get(x_4, 0);
x_27 = lean_ctor_get(x_5, 2);
lean_inc(x_27);
x_28 = lean_ctor_get(x_4, 1);
x_28 = lean_ctor_get(x_5, 3);
lean_inc(x_28);
x_29 = lean_ctor_get(x_4, 2);
lean_inc(x_29);
x_30 = lean_ctor_get(x_4, 3);
lean_inc(x_30);
if (lean_is_exclusive(x_4)) {
lean_ctor_release(x_4, 0);
lean_ctor_release(x_4, 1);
lean_ctor_release(x_4, 2);
lean_ctor_release(x_4, 3);
lean_ctor_release(x_4, 4);
x_31 = x_4;
if (lean_is_exclusive(x_5)) {
lean_ctor_release(x_5, 0);
lean_ctor_release(x_5, 1);
lean_ctor_release(x_5, 2);
lean_ctor_release(x_5, 3);
lean_ctor_release(x_5, 4);
x_29 = x_5;
} else {
lean_dec_ref(x_4);
lean_dec_ref(x_5);
x_29 = lean_box(0);
}
x_30 = lean_ctor_get(x_24, 0);
lean_inc(x_30);
if (lean_is_exclusive(x_24)) {
lean_ctor_release(x_24, 0);
lean_ctor_release(x_24, 1);
x_31 = x_24;
} else {
lean_dec_ref(x_24);
x_31 = lean_box(0);
}
x_32 = lean_ctor_get(x_26, 0);
lean_inc(x_32);
if (lean_is_exclusive(x_26)) {
lean_ctor_release(x_26, 0);
lean_ctor_release(x_26, 1);
x_33 = x_26;
} else {
lean_dec_ref(x_26);
x_33 = lean_box(0);
}
x_34 = lean_box(0);
if (lean_is_scalar(x_33)) {
x_35 = lean_alloc_ctor(0, 2, 0);
} else {
x_35 = x_33;
}
lean_ctor_set(x_35, 0, x_32);
lean_ctor_set(x_35, 1, x_34);
x_36 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_36, 0, x_35);
if (lean_is_scalar(x_31)) {
x_37 = lean_alloc_ctor(0, 5, 0);
x_32 = lean_alloc_ctor(0, 2, 0);
} else {
x_37 = x_31;
x_32 = x_31;
}
lean_ctor_set(x_37, 0, x_27);
lean_ctor_set(x_37, 1, x_28);
lean_ctor_set(x_37, 2, x_29);
lean_ctor_set(x_37, 3, x_30);
lean_ctor_set(x_37, 4, x_36);
return x_37;
lean_ctor_set(x_32, 0, x_30);
lean_ctor_set(x_32, 1, x_1);
x_33 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_33, 0, x_32);
if (lean_is_scalar(x_29)) {
x_34 = lean_alloc_ctor(0, 5, 0);
} else {
x_34 = x_29;
}
lean_ctor_set(x_34, 0, x_25);
lean_ctor_set(x_34, 1, x_26);
lean_ctor_set(x_34, 2, x_27);
lean_ctor_set(x_34, 3, x_28);
lean_ctor_set(x_34, 4, x_33);
return x_34;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_setExpectedFn(lean_object* x_1) {
LEAN_EXPORT lean_object* l_Lean_Parser_setExpected___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_setExpectedFn___rarg), 3, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_setExpectedFn___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Parser_setExpectedFn(x_1);
lean_dec(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_setExpected___elambda__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Parser_setExpectedFn___rarg(x_1, x_2, x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_setExpected___elambda__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Parser_setExpected___elambda__1___rarg), 3, 0);
return x_2;
lean_object* x_5;
x_5 = l_Lean_Parser_setExpectedFn(x_1, x_2, x_3, x_4);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_setExpected(lean_object* x_1, lean_object* x_2) {
@ -26985,8 +26952,9 @@ if (x_3 == 0)
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_ctor_get(x_2, 1);
x_5 = lean_alloc_closure((void*)(l_Lean_Parser_setExpected___elambda__1___rarg), 3, 1);
lean_closure_set(x_5, 0, x_4);
x_5 = lean_alloc_closure((void*)(l_Lean_Parser_setExpected___elambda__1), 4, 2);
lean_closure_set(x_5, 0, x_1);
lean_closure_set(x_5, 1, x_4);
lean_ctor_set(x_2, 1, x_5);
return x_2;
}
@ -26998,8 +26966,9 @@ x_7 = lean_ctor_get(x_2, 1);
lean_inc(x_7);
lean_inc(x_6);
lean_dec(x_2);
x_8 = lean_alloc_closure((void*)(l_Lean_Parser_setExpected___elambda__1___rarg), 3, 1);
lean_closure_set(x_8, 0, x_7);
x_8 = lean_alloc_closure((void*)(l_Lean_Parser_setExpected___elambda__1), 4, 2);
lean_closure_set(x_8, 0, x_1);
lean_closure_set(x_8, 1, x_7);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_6);
lean_ctor_set(x_9, 1, x_8);
@ -27007,24 +26976,6 @@ return x_9;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_setExpected___elambda__1___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Parser_setExpected___elambda__1(x_1);
lean_dec(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_Parser_setExpected___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Parser_setExpected(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_Parser_pushNone___elambda__1___rarg___closed__1() {
_start:
{

416
stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c generated
View file

@ -36,6 +36,7 @@ LEAN_EXPORT lean_object* l_panic___at_Lean_PrettyPrinter_Delaborator_withMDataOp
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabDIte___closed__4;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabDIte___closed__1;
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabCond___closed__1;
uint8_t lean_local_ctx_uses_user_name(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_unresolveNameGlobal_unresolveNameCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabProj___closed__2;
@ -57,6 +58,7 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppImplicit___lambda__
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLam___lambda__3___closed__4;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabConst___closed__1;
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_delabDoElems___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__2;
lean_object* lean_erase_macro_scopes(lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNameMkStr(lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withMDataExpr___at_Lean_PrettyPrinter_Delaborator_withMDataOptions___spec__2___rarg___closed__1;
@ -71,6 +73,7 @@ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch___lambda
static lean_object* l_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance___lambda__3___closed__5;
lean_object* lean_local_ctx_get_unused_name(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabLetE___closed__1;
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__1;
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabDIte___closed__1;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLam___lambda__3___closed__9;
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
@ -149,6 +152,7 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_isRegularApp___lambda__4___
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch___lambda__6___closed__6;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__11___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__8;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppMatch(lean_object*);
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_nextExtraPos___at_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance___spec__1(lean_object*);
@ -187,6 +191,7 @@ lean_object* l_List_tailD___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabConst___spec__1___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_withMDataOptions(lean_object*);
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabFVar___closed__8;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetE(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabLit(lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
@ -203,6 +208,7 @@ LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_PrettyPrinter_Delabora
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_nextExtraPos___at_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfScientific___closed__5;
LEAN_EXPORT lean_object* l_panic___at_Lean_PrettyPrinter_Delaborator_withMDataOptions___spec__6___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabCond___closed__2;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabDo(lean_object*);
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNameMkStr___closed__5;
lean_object* l_Lean_Expr_appFn_x21(lean_object*);
@ -242,6 +248,7 @@ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_reifyName___boxed(lean
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabForall___closed__2;
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabSigma___closed__4;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabDo___lambda__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Name_isPrefixOf(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_withMDataOptions___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_getExpr___at_Lean_PrettyPrinter_Delaborator_getExprKind___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -253,6 +260,7 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_delabMVar___closed__4;
static lean_object* l_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance___lambda__3___closed__7;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabNameMkStr___lambda__1___closed__2;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabNameMkStr___closed__1;
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabCond(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_shrink___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_unfoldMDatas___boxed(lean_object*);
uint8_t l_Lean_PrettyPrinter_Delaborator_isCoe(lean_object*);
@ -291,6 +299,7 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_delabMData___closed__2;
extern lean_object* l_Lean_nameLitKind;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabDoElems___closed__4;
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabSigma___closed__2;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__2;
static lean_object* l_Lean_PrettyPrinter_Delaborator_reifyName___closed__4;
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabLam___closed__1;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance___spec__7(lean_object*, lean_object*, size_t, size_t, lean_object*);
@ -335,6 +344,7 @@ LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_PrettyPrinter_Delabora
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabMVar___closed__3;
static lean_object* l_Std_Range_forIn_loop___at_Lean_PrettyPrinter_Delaborator_isRegularApp___spec__3___closed__4;
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabDo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond(lean_object*);
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfScientific___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabLam___closed__5;
@ -373,6 +383,7 @@ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lam
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__17___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_PrettyPrinter_Delaborator_hasIdent___spec__1(lean_object*, lean_object*, size_t, size_t);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__4___closed__6;
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__3;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetFun___lambda__1___closed__6;
lean_object* l_Lean_PrettyPrinter_Delaborator_annotateCurPos(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_reifyName___closed__2;
@ -404,6 +415,7 @@ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_unexpandStructureInsta
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabDoElems___closed__5;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch___lambda__6___closed__7;
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__5;
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabDIte___closed__3;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_PrettyPrinter_Delaborator_unresolveNameGlobal___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*, lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabMData___closed__1;
@ -583,6 +595,7 @@ lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_
uint8_t l_Lean_Expr_isConst(lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabSort___closed__9;
uint8_t l_Array_isEmpty___rarg(lean_object*);
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__3;
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfNat___closed__3;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetFun___lambda__1___closed__5;
extern lean_object* l_Lean_instInhabitedSyntax;
@ -865,6 +878,7 @@ extern lean_object* l_Lean_PrettyPrinter_Delaborator_appUnexpanderAttribute;
static lean_object* l_Lean_getConstInfo___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__2___closed__2;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabDoElems___lambda__6___closed__2;
lean_object* lean_panic_fn(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__4;
static lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch___lambda__6___closed__1;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabBVar(lean_object*);
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -27580,6 +27594,383 @@ x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("boolIfThenElse");
return x_1;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("bif");
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabCond___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) {
_start:
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12; lean_object* x_13;
x_9 = lean_unsigned_to_nat(0u);
x_10 = l_Lean_Expr_getAppNumArgsAux(x_1, x_9);
x_11 = lean_unsigned_to_nat(4u);
x_12 = lean_nat_dec_eq(x_10, x_11);
lean_dec(x_10);
if (x_12 == 0)
{
lean_object* x_77; uint8_t x_78;
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_77 = l_Lean_PrettyPrinter_Delaborator_failure___rarg(x_8);
x_78 = !lean_is_exclusive(x_77);
if (x_78 == 0)
{
return x_77;
}
else
{
lean_object* x_79; lean_object* x_80; lean_object* x_81;
x_79 = lean_ctor_get(x_77, 0);
x_80 = lean_ctor_get(x_77, 1);
lean_inc(x_80);
lean_inc(x_79);
lean_dec(x_77);
x_81 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_81, 0, x_79);
lean_ctor_set(x_81, 1, x_80);
return x_81;
}
}
else
{
x_13 = x_8;
goto block_76;
}
block_76:
{
lean_object* x_14; lean_object* x_15;
x_14 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__2;
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
x_15 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabLetFun___spec__4(x_14, x_2, x_3, x_4, x_5, x_6, x_7, x_13);
if (lean_obj_tag(x_15) == 0)
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_16 = lean_ctor_get(x_15, 0);
lean_inc(x_16);
x_17 = lean_ctor_get(x_15, 1);
lean_inc(x_17);
lean_dec(x_15);
x_18 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__1;
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
x_19 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabLetFun___spec__4(x_18, x_2, x_3, x_4, x_5, x_6, x_7, x_17);
if (lean_obj_tag(x_19) == 0)
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_20 = lean_ctor_get(x_19, 0);
lean_inc(x_20);
x_21 = lean_ctor_get(x_19, 1);
lean_inc(x_21);
lean_dec(x_19);
x_22 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__4___closed__2;
lean_inc(x_7);
lean_inc(x_6);
x_23 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabLetFun___spec__1(x_22, x_2, x_3, x_4, x_5, x_6, x_7, x_21);
if (lean_obj_tag(x_23) == 0)
{
lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27;
x_24 = lean_ctor_get(x_23, 0);
lean_inc(x_24);
x_25 = lean_ctor_get(x_23, 1);
lean_inc(x_25);
lean_dec(x_23);
x_26 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_PrettyPrinter_Delaborator_delab___spec__3___rarg(x_6, x_7, x_25);
lean_dec(x_7);
x_27 = !lean_is_exclusive(x_26);
if (x_27 == 0)
{
lean_object* x_28; lean_object* x_29; 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; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44;
x_28 = lean_ctor_get(x_26, 0);
x_29 = l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__3;
lean_inc(x_28);
x_30 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_30, 0, x_28);
lean_ctor_set(x_30, 1, x_29);
x_31 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__6;
lean_inc(x_28);
x_32 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_32, 0, x_28);
lean_ctor_set(x_32, 1, x_31);
x_33 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__7;
x_34 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_34, 0, x_28);
lean_ctor_set(x_34, 1, x_33);
x_35 = l_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance___lambda__3___closed__13;
x_36 = lean_array_push(x_35, x_30);
x_37 = lean_array_push(x_36, x_16);
x_38 = lean_array_push(x_37, x_32);
x_39 = lean_array_push(x_38, x_20);
x_40 = lean_array_push(x_39, x_34);
x_41 = lean_array_push(x_40, x_24);
x_42 = lean_box(2);
x_43 = l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__2;
x_44 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_44, 0, x_42);
lean_ctor_set(x_44, 1, x_43);
lean_ctor_set(x_44, 2, x_41);
lean_ctor_set(x_26, 0, x_44);
return x_26;
}
else
{
lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63;
x_45 = lean_ctor_get(x_26, 0);
x_46 = lean_ctor_get(x_26, 1);
lean_inc(x_46);
lean_inc(x_45);
lean_dec(x_26);
x_47 = l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__3;
lean_inc(x_45);
x_48 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_48, 0, x_45);
lean_ctor_set(x_48, 1, x_47);
x_49 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__6;
lean_inc(x_45);
x_50 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_50, 0, x_45);
lean_ctor_set(x_50, 1, x_49);
x_51 = l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__7;
x_52 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_52, 0, x_45);
lean_ctor_set(x_52, 1, x_51);
x_53 = l_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance___lambda__3___closed__13;
x_54 = lean_array_push(x_53, x_48);
x_55 = lean_array_push(x_54, x_16);
x_56 = lean_array_push(x_55, x_50);
x_57 = lean_array_push(x_56, x_20);
x_58 = lean_array_push(x_57, x_52);
x_59 = lean_array_push(x_58, x_24);
x_60 = lean_box(2);
x_61 = l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__2;
x_62 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_62, 0, x_60);
lean_ctor_set(x_62, 1, x_61);
lean_ctor_set(x_62, 2, x_59);
x_63 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_63, 0, x_62);
lean_ctor_set(x_63, 1, x_46);
return x_63;
}
}
else
{
uint8_t x_64;
lean_dec(x_20);
lean_dec(x_16);
lean_dec(x_7);
lean_dec(x_6);
x_64 = !lean_is_exclusive(x_23);
if (x_64 == 0)
{
return x_23;
}
else
{
lean_object* x_65; lean_object* x_66; lean_object* x_67;
x_65 = lean_ctor_get(x_23, 0);
x_66 = lean_ctor_get(x_23, 1);
lean_inc(x_66);
lean_inc(x_65);
lean_dec(x_23);
x_67 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_67, 0, x_65);
lean_ctor_set(x_67, 1, x_66);
return x_67;
}
}
}
else
{
uint8_t x_68;
lean_dec(x_16);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_68 = !lean_is_exclusive(x_19);
if (x_68 == 0)
{
return x_19;
}
else
{
lean_object* x_69; lean_object* x_70; lean_object* x_71;
x_69 = lean_ctor_get(x_19, 0);
x_70 = lean_ctor_get(x_19, 1);
lean_inc(x_70);
lean_inc(x_69);
lean_dec(x_19);
x_71 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_71, 0, x_69);
lean_ctor_set(x_71, 1, x_70);
return x_71;
}
}
}
else
{
uint8_t x_72;
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_72 = !lean_is_exclusive(x_15);
if (x_72 == 0)
{
return x_15;
}
else
{
lean_object* x_73; lean_object* x_74; lean_object* x_75;
x_73 = lean_ctor_get(x_15, 0);
x_74 = lean_ctor_get(x_15, 1);
lean_inc(x_74);
lean_inc(x_73);
lean_dec(x_15);
x_75 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_75, 0, x_73);
lean_ctor_set(x_75, 1, x_74);
return x_75;
}
}
}
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabCond___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___boxed), 8, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabCond___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_PrettyPrinter_Delaborator_unexpandCoe___closed__1;
x_2 = l_Lean_PrettyPrinter_Delaborator_delabCond___closed__1;
x_3 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_PrettyPrinter_Delaborator_delabAppExplicit___spec__1___rarg), 9, 2);
lean_closure_set(x_3, 0, x_1);
lean_closure_set(x_3, 1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabCond(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_8 = l_Lean_PrettyPrinter_Delaborator_delabAppImplicit___lambda__3___closed__2;
x_9 = l_Lean_PrettyPrinter_Delaborator_delabCond___closed__2;
x_10 = l_Lean_PrettyPrinter_Delaborator_whenPPOption(x_8, x_9, x_1, x_2, x_3, x_4, x_5, x_6, x_7);
return x_10;
}
}
LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabCond___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* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9;
x_9 = l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_1);
return x_9;
}
}
static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("cond");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppExplicit___closed__2;
x_2 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("delabCond");
return x_1;
}
}
static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabFVar___closed__6;
x_2 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__3;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_delabCond), 7, 0);
return x_1;
}
}
LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond(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;
x_2 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabFVar___closed__9;
x_3 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__2;
x_4 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__4;
x_5 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__5;
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1() {
_start:
{
@ -29674,7 +30065,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_PrettyPrinter_Delaborator_delabFVar___closed__1;
x_2 = l_Lean_PrettyPrinter_Delaborator_delabDoElems___closed__5;
x_3 = lean_unsigned_to_nat(739u);
x_3 = lean_unsigned_to_nat(747u);
x_4 = lean_unsigned_to_nat(40u);
x_5 = l_Lean_PrettyPrinter_Delaborator_delabFVar___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -32107,6 +32498,29 @@ lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabDIte___c
res = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabDIte(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__1 = _init_l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__1();
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__1);
l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__2 = _init_l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__2();
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__2);
l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__3 = _init_l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__3();
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabCond___lambda__1___closed__3);
l_Lean_PrettyPrinter_Delaborator_delabCond___closed__1 = _init_l_Lean_PrettyPrinter_Delaborator_delabCond___closed__1();
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabCond___closed__1);
l_Lean_PrettyPrinter_Delaborator_delabCond___closed__2 = _init_l_Lean_PrettyPrinter_Delaborator_delabCond___closed__2();
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabCond___closed__2);
l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__1 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__1);
l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__2 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__2);
l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__3 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__3();
lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__3);
l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__4 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__4();
lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__4);
l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__5 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__5();
lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond___closed__5);
res = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabCond(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1 = _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1();
lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1);
l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2 = _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2();