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:
Gabriel Ebner 2021-10-26 10:53:35 +02:00 • committed by Sebastian Ullrich
parent 6063c662de
commit aa3d7cd751
30 changed files with 15544 additions and 14414 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -24,6 +24,7 @@ import Lean.Elab.Inductive
import Lean.Elab.Structure
import Lean.Elab.Print
import Lean.Elab.MutualDef
import Lean.Elab.AuxDef
import Lean.Elab.PreDefinition
import Lean.Elab.Deriving
import Lean.Elab.DeclarationRange

32
stage0/src/Lean/Elab/AuxDef.lean generated Normal file
View file

@ -0,0 +1,32 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner
-/
import Lean.Elab.Command
namespace Lean.Elab.Command
open Lean.Parser.Command
open Lean.Parser.Term
/--
Declares an auxiliary definition with an automatically generated name.
For example, `aux_def foo : Nat := 42` creates a definition
with an internal, unused name based on the suggestion `foo`.
-/
scoped syntax (name := aux_def) docComment ? attributes ? "aux_def" ident+ ":" term ":=" term : command
@[builtinCommandElab «aux_def»]
def elabAuxDef : CommandElab
| `($[$doc?:docComment]? $[$attrs?:attributes]? aux_def $[$suggestion:ident]* : $ty := $body) => do
let id := suggestion.map (·.getId.eraseMacroScopes) |>.foldl (· ++ ·) Name.anonymous
let id := `_aux ++ (← getMainModule) ++ `_ ++ id
let id := String.intercalate "_" <| id.components.map (·.toString)
let ns ← getCurrNamespace
-- make sure we only add a single component so that scoped workes
let id ← mkAuxName (ns.mkStr id) 1
let id := id.replacePrefix ns Name.anonymous -- TODO: replace with def _root_.id
elabCommand <|
← `($[$doc?:docComment]? $[$attrs?:attributes]?
def $(mkIdent id):ident : $ty := $body)
| _ => throwUnsupportedSyntax

13
stage0/src/Lean/Elab/ElabRules.lean generated
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Elab.MacroArgUtil
import Lean.Elab.AuxDef
namespace Lean.Elab.Command
open Lean.Syntax
@ -42,20 +43,24 @@ def elabElabRulesAux (doc? : Option Syntax) (attrKind : Syntax) (k : SyntaxNodeK
| _, _ => throwError "invalid elab_rules command, specify category using `elab_rules : <cat> ...`"
if let some expId := expty? then
if catName == `term then
`($[$doc?:docComment]? @[termElab $(← mkIdentFromRef k):ident] def elabFn : Lean.Elab.Term.TermElab :=
`($[$doc?:docComment]? @[termElab $(← mkIdentFromRef k):ident]
aux_def elabRules $(mkIdent k) : Lean.Elab.Term.TermElab :=
fun stx expectedType? => Lean.Elab.Command.withExpectedType expectedType? fun $expId => match stx with
$alts:matchAlt* | _ => throwUnsupportedSyntax)
else
throwErrorAt expId "syntax category '{catName}' does not support expected type specification"
else if catName == `term then
`($[$doc?:docComment]? @[termElab $(← mkIdentFromRef k):ident] def elabFn : Lean.Elab.Term.TermElab :=
`($[$doc?:docComment]? @[termElab $(← mkIdentFromRef k):ident]
aux_def elabRules $(mkIdent k) : Lean.Elab.Term.TermElab :=
fun stx _ => match stx with
$alts:matchAlt* | _ => throwUnsupportedSyntax)
else if catName == `command then
`($[$doc?:docComment]? @[commandElab $(← mkIdentFromRef k):ident] def elabFn : Lean.Elab.Command.CommandElab :=
`($[$doc?:docComment]? @[commandElab $(← mkIdentFromRef k):ident]
aux_def elabRules $(mkIdent k) : Lean.Elab.Command.CommandElab :=
fun $alts:matchAlt* | _ => throwUnsupportedSyntax)
else if catName == `tactic then
`($[$doc?:docComment]? @[tactic $(← mkIdentFromRef k):ident] def elabFn : Lean.Elab.Tactic.Tactic :=
`($[$doc?:docComment]? @[tactic $(← mkIdentFromRef k):ident]
aux_def elabRules $(mkIdent k) : Lean.Elab.Tactic.Tactic :=
fun $alts:matchAlt* | _ => throwUnsupportedSyntax)
else
-- We considered making the command extensible and support new user-defined categories. We think it is unnecessary.

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

@ -127,12 +127,13 @@ private partial def checkParamsAndResultType (type firstType : Expr) (numParams
forallTelescopeCompatible type firstType numParams fun _ type firstType =>
forallTelescopeReducing type fun _ type =>
forallTelescopeReducing firstType fun _ firstType => do
match type with
| Expr.sort .. =>
unless (← isDefEq firstType type) do
throwError "resulting universe mismatch, given{indentExpr type}\nexpected type{indentExpr firstType}"
| _ =>
throwError "unexpected inductive resulting type"
let type ← whnfD type
match type with
| Expr.sort .. =>
unless (← isDefEq firstType type) do
throwError "resulting universe mismatch, given{indentExpr type}\nexpected type{indentExpr firstType}"
| _ =>
throwError "unexpected inductive resulting type"
catch
| Exception.error ref msg => throw (Exception.error ref m!"invalid mutually inductive types, {msg}")
| ex => throw ex
@ -257,9 +258,10 @@ private def levelMVarToParam (indTypes : List InductiveType) : TermElabM (List I
private def getResultingUniverse : List InductiveType → TermElabM Level
| [] => throwError "unexpected empty inductive declaration"
| indType :: _ => forallTelescopeReducing indType.type fun _ r => do
let r ← whnfD r
match r with
| Expr.sort u _ => pure u
| _ => throwError "unexpected inductive type resulting type"
| _ => throwError "unexpected inductive type resulting type{indentExpr r}"
def tmpIndParam := mkLevelParam `_tmp_ind_univ_param
@ -492,6 +494,7 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
| Except.ok levelParams => do
let indTypes ← replaceIndFVarsWithConsts views indFVars levelParams numVars numParams indTypes
let indTypes := applyInferMod views numParams indTypes
trace[Meta.debug] "levelParams: {levelParams}"
let decl := Declaration.inductDecl levelParams numParams indTypes isUnsafe
Term.ensureNoUnassignedMVars decl
addDecl decl

7
stage0/src/Lean/Elab/MacroRules.lean generated
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Elab.Syntax
import Lean.Elab.AuxDef
namespace Lean.Elab.Command
open Lean.Syntax
@ -34,7 +35,8 @@ def elabMacroRulesAux (doc? : Option Syntax) (attrKind : Syntax) (k : SyntaxNode
else
throwErrorAt alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
| _ => throwUnsupportedSyntax
`($[$doc?:docComment]? @[$attrKind:attrKind macro $(Lean.mkIdent k)] def myMacro : Macro :=
`($[$doc?:docComment]? @[$attrKind:attrKind macro $(Lean.mkIdent k)]
aux_def macroRules $(mkIdent k) : Macro :=
fun $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
@[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
@ -43,7 +45,8 @@ def elabMacroRulesAux (doc? : Option Syntax) (attrKind : Syntax) (k : SyntaxNode
expandNoKindMacroRulesAux alts "macro_rules" fun kind? alts =>
`($[$doc?:docComment]? $attrKind:attrKind macro_rules $[(kind := $(mkIdent <$> kind?))]? $alts:matchAlt*)
| `($[$doc?:docComment]? $attrKind:attrKind macro_rules (kind := $kind) | $x:ident => $rhs) =>
`($[$doc?:docComment]? @[$attrKind:attrKind macro $kind] def myMacro : Macro := fun $x:ident => $rhs)
`($[$doc?:docComment]? @[$attrKind:attrKind macro $kind]
aux_def macroRules $kind : Macro := fun $x:ident => $rhs)
| `($[$doc?:docComment]? $attrKind:attrKind macro_rules (kind := $kind) $alts:matchAlt*) =>
do elabMacroRulesAux doc? attrKind (← resolveSyntaxKind kind.getId) alts
| _ => throwUnsupportedSyntax

7
stage0/src/Lean/Elab/Notation.lean generated
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Elab.Syntax
import Lean.Elab.AuxDef
namespace Lean.Elab.Command
open Lean.Syntax
@ -52,12 +53,14 @@ def mkSimpleDelab (attrKind : Syntax) (vars : Array Syntax) (pat qrhs : Syntax)
guard <| args.all (Syntax.isIdent ∘ getAntiquotTerm)
guard <| args.allDiff
-- replace head constant with (unused) antiquotation so we're not dependent on the exact pretty printing of the head
`(@[$attrKind:attrKind appUnexpander $(mkIdent c):ident] def unexpand : Lean.PrettyPrinter.Unexpander := fun
`(@[$attrKind:attrKind appUnexpander $(mkIdent c):ident]
aux_def unexpand $(mkIdent c) : Lean.PrettyPrinter.Unexpander := fun
| `($$(_):ident $args*) => `($pat)
| _ => throw ())
| `($c:ident) =>
let [(c, [])] ← Macro.resolveGlobalName c.getId | failure
`(@[$attrKind:attrKind appUnexpander $(mkIdent c):ident] def unexpand : Lean.PrettyPrinter.Unexpander
`(@[$attrKind:attrKind appUnexpander $(mkIdent c):ident]
aux_def unexpand $(mkIdent c) : Lean.PrettyPrinter.Unexpander := fun
| `($$(_):ident) => `($pat)
| _ => throw ())
| _ => failure

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

@ -1146,6 +1146,16 @@ def sortFVarIds (fvarIds : Array FVarId) : MetaM (Array FVarId) := do
| none, none => Name.quickLt fvarId₁.name fvarId₂.name
end Methods
def isInductivePredicate (declName : Name) : MetaM Bool := do
match (← getEnv).find? declName with
| some (ConstantInfo.inductInfo { type := type, ..}) =>
forallTelescopeReducing type fun _ type => do
match (← whnfD type) with
| Expr.sort u .. => return u == levelZero
| _ => return false
| _ => return false
end Meta
export Meta (MetaM)

95
stage0/src/Lean/Meta/IndPredBelow.lean generated
View file

@ -55,15 +55,16 @@ def mkContext (declName : Name) : MetaM Context := do
let indVal ← getConstInfoInduct declName
let typeInfos ← indVal.all.toArray.mapM getConstInfoInduct
let motiveTypes ← typeInfos.mapM motiveType
let motives ←motiveTypes.mapIdxM fun j motive => do
(←motiveName motiveTypes j.val, motive)
let headers := typeInfos.mapM $ mkHeader motives indVal.numParams
let motives ← motiveTypes.mapIdxM fun j motive => do
(← motiveName motiveTypes j.val, motive)
let headers ← typeInfos.mapM $ mkHeader motives indVal.numParams
return {
motives := motives
typeInfos := typeInfos
numParams := indVal.numParams
headers := ←headers
belowNames := ←indVal.all.toArray.map (· ++ `below) }
headers := headers
belowNames := (← indVal.all.toArray.map (· ++ `below))
}
where
motiveName (motiveTypes : Array Expr) (i : Nat) : MetaM Name :=
if motiveTypes.size > 1
@ -74,21 +75,21 @@ where
(motives : Array (Name × Expr))
(numParams : Nat)
(indVal : InductiveVal) : MetaM Expr := do
let header ← forallTelescope indVal.type fun xs t => do
let header ← forallTelescopeReducing indVal.type fun xs t => do
withNewBinderInfos (xs.map fun x => (x.fvarId!, BinderInfo.implicit)) $
mkForallFVars xs $ ←mkArrow (mkAppN (mkIndValConst indVal) xs) t
mkForallFVars xs (← mkArrow (mkAppN (mkIndValConst indVal) xs) t)
addMotives motives numParams header
addMotives (motives : Array (Name × Expr)) (numParams : Nat) : Expr → MetaM Expr :=
motives.foldrM (fun (motiveName, motive) t =>
forallTelescope t fun xs s => do
forallTelescopeReducing t fun xs s => do
let motiveType ← instantiateForall motive xs[:numParams]
withLocalDecl motiveName BinderInfo.implicit motiveType fun motive => do
mkForallFVars (xs.insertAt numParams motive) s)
motiveType (indVal : InductiveVal) : MetaM Expr :=
forallTelescope indVal.type fun xs t => do
mkForallFVars xs $ ←mkArrow (mkAppN (mkIndValConst indVal) xs) (mkSort levelZero)
forallTelescopeReducing indVal.type fun xs t => do
mkForallFVars xs (← mkArrow (mkAppN (mkIndValConst indVal) xs) (mkSort levelZero))
mkIndValConst (indVal : InductiveVal) : Expr :=
mkConst indVal.name $ indVal.levelParams.map mkLevelParam
@ -97,7 +98,7 @@ partial def mkCtorType
(ctx : Context)
(belowIdx : Nat)
(originalCtor : ConstructorVal) : MetaM Expr :=
forallTelescope originalCtor.type fun xs t => addHeaderVars
forallTelescopeReducing originalCtor.type fun xs t => addHeaderVars
{ innerType := t
indVal := #[]
motives := #[]
@ -122,8 +123,8 @@ where
modifyBinders (vars : Variables) (i : Nat) := do
if i < vars.args.size then
let binder := vars.args[i]
let binderType ←inferType binder
if ←checkCount binderType then
let binderType ← inferType binder
if (← checkCount binderType) then
mkBelowBinder vars binder binderType fun indValIdx x =>
mkMotiveBinder vars indValIdx binder binderType fun y =>
withNewBinderInfos #[(binder.fvarId!, BinderInfo.implicit)] do
@ -151,11 +152,10 @@ where
checkCount (domain : Expr) : MetaM Bool := do
let run (x : StateRefT Nat MetaM Expr) : MetaM (Expr × Nat) := StateRefT'.run x 0
let (_, cnt) ←run $ transform domain fun e => do
let (_, cnt) ← run $ transform domain fun e => do
if let some name := e.constName? then
if let some idx := ctx.typeInfos.findIdx? fun indVal => indVal.name == name then
let cnt ←get
set $ cnt + 1
modify (. + 1)
TransformStep.visit e
if cnt > 1 then
@ -168,7 +168,7 @@ where
(binder : Expr)
(domain : Expr)
{α : Type} (k : Nat → Expr → MetaM α) : MetaM α := do
forallTelescope domain fun xs t => do
forallTelescopeReducing domain fun xs t => do
let fail _ := do
throwError "only trivial inductive applications supported in premises:{indentExpr t}"
@ -193,7 +193,7 @@ where
(binder : Expr)
(domain : Expr)
{α : Type} (k : Expr → MetaM α) : MetaM α := do
forallTelescope domain fun xs t => do
forallTelescopeReducing domain fun xs t => do
t.withApp fun f args => do
let hApp := mkAppN binder xs
let t := mkAppN vars.motives[indValIdx] $ args[ctx.numParams:] ++ #[hApp]
@ -220,7 +220,8 @@ def mkInductiveType
return {
name := ctx.belowNames[i]
type := ctx.headers[i]
ctors := ←indVal.ctors.mapM (mkConstructor ctx i) }
ctors := (← indVal.ctors.mapM (mkConstructor ctx i))
}
def mkBelowDecl (ctx : Context) : MetaM Declaration := do
let lparams := ctx.typeInfos[0].levelParams
@ -268,8 +269,8 @@ where
return (m, ⟨params, motives, indices, witness, indHyps⟩)
applyIH (m : MVarId) (vars : BrecOnVariables) : MetaM (List MVarId) := do
match ←vars.indHyps.findSomeM?
(fun ih => do try some $ (←apply m $ mkFVar ih) catch ex => none) with
match (← vars.indHyps.findSomeM?
fun ih => do try some $ (←apply m $ mkFVar ih) catch ex => none) with
| some goals => goals
| none => throwError "cannot apply induction hypothesis: {MessageData.ofGoal m}"
@ -279,7 +280,7 @@ where
let levelParams := indVal.levelParams.map mkLevelParam
let motives ← ctx.motives.mapIdxM fun idx (_, motive) => do
let motive ← instantiateForall motive params
forallTelescope motive fun xs _ => do
forallTelescopeReducing motive fun xs _ => do
mkLambdaFVars xs $ mkAppN (mkConst ctx.belowNames[idx] levelParams) $ (params ++ motives ++ xs)
let recursorInfo ← getConstInfo $ mkRecName indVal.name
let recLevels :=
@ -292,24 +293,24 @@ where
applyCtors (ms : List MVarId) : MetaM $ List MVarId := do
let mss ← ms.toArray.mapIdxM fun idx m => do
let m ← introNPRec m
(←getMVarType m).withApp fun below args =>
(← getMVarType m).withApp fun below args =>
withMVarContext m do
args.back.withApp fun ctor ctorArgs => do
let ctorName := ctor.constName!.updatePrefix below.constName!
let ctor := mkConst ctorName below.constLevels!
let ctorInfo ← getConstInfoCtor ctorName
let (mvars, _, t) ← forallMetaTelescope ctorInfo.type
let ctor := mkAppN ctor mvars
apply m ctor
args.back.withApp fun ctor ctorArgs => do
let ctorName := ctor.constName!.updatePrefix below.constName!
let ctor := mkConst ctorName below.constLevels!
let ctorInfo ← getConstInfoCtor ctorName
let (mvars, _, t) ← forallMetaTelescope ctorInfo.type
let ctor := mkAppN ctor mvars
apply m ctor
return mss.foldr List.append []
introNPRec (m : MVarId) : MetaM MVarId := do
if (←getMVarType m).isForall then introNPRec (←intro1P m).2 else m
if (← getMVarType m).isForall then introNPRec (←intro1P m).2 else m
closeGoal (vars : BrecOnVariables) (maxDepth : Nat) (m : MVarId) : MetaM Unit := do
unless ←isExprMVarAssigned m do
unless (← isExprMVarAssigned m) do
let m ← introNPRec m
unless ←backwardsChaining m maxDepth do
unless (← backwardsChaining m maxDepth) do
withMVarContext m do
throwError "couldn't solve by backwards chaining ({``maxBackwardChainingDepth} = {maxDepth}): {MessageData.ofGoal m}"
@ -324,7 +325,7 @@ def mkBrecOnDecl (ctx : Context) (idx : Nat) : MetaM Declaration := do
value := ←proveBrecOn ctx indVal type }
where
mkType : MetaM Expr :=
forallTelescope ctx.headers[idx] fun xs t => do
forallTelescopeReducing ctx.headers[idx] fun xs t => do
let params := xs[:ctx.numParams]
let motives := xs[ctx.numParams:ctx.numParams + ctx.motives.size].toArray
let indices := xs[ctx.numParams + ctx.motives.size:]
@ -342,7 +343,7 @@ where
else mkFreshUserName "ih"
let ih ← instantiateForall motive.2 params
let mkDomain (_ : Array Expr) : MetaM Expr :=
forallTelescope ih fun ys t => do
forallTelescopeReducing ih fun ys t => do
let levels := ctx.typeInfos[idx].levelParams.map mkLevelParam
let args := params ++ motives ++ ys
let premise :=
@ -358,7 +359,7 @@ partial def getBelowIndices (ctorName : Name) : MetaM $ Array Nat := do
let ctorInfo ← getConstInfoCtor ctorName
let belowCtorInfo ← getConstInfoCtor (ctorName.updatePrefix $ ctorInfo.induct ++ `below)
let belowInductInfo ← getConstInfoInduct belowCtorInfo.induct
forallTelescope ctorInfo.type fun xs t => do
forallTelescopeReducing ctorInfo.type fun xs t => do
loop xs belowCtorInfo.type #[] 0 0
where
@ -371,7 +372,7 @@ where
let x := xs[xIdx]
let xTy ← inferType x
let yTy := rest.bindingDomain!
if ←isDefEq xTy yTy then
if (← isDefEq xTy yTy) then
let rest ← instantiateForall rest #[x]
loop xs rest (belowIndices.push yIdx) (xIdx + 1) (yIdx + 1)
else
@ -379,12 +380,12 @@ where
loop xs rest belowIndices xIdx (yIdx + 1)
private def belowType (motive : Expr) (xs : Array Expr) (idx : Nat) : MetaM $ Name × Expr := do
(←inferType xs[idx]).withApp fun type args => do
let indName := type.constName!
let indInfo ← getConstInfoInduct indName
let belowArgs := args[:indInfo.numParams] ++ #[motive] ++ args[indInfo.numParams:] ++ #[xs[idx]]
let belowType := mkAppN (mkConst (indName ++ `below) type.constLevels!) belowArgs
(indName, belowType)
(← inferType xs[idx]).withApp fun type args => do
let indName := type.constName!
let indInfo ← getConstInfoInduct indName
let belowArgs := args[:indInfo.numParams] ++ #[motive] ++ args[indInfo.numParams:] ++ #[xs[idx]]
let belowType := mkAppN (mkConst (indName ++ `below) type.constLevels!) belowArgs
(indName, belowType)
/-- This function adds an additional `below` discriminant to a matcher application.
It is used for modifying the patterns, such that the structural recursion can use the new
@ -562,14 +563,14 @@ def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat
xTy.withApp fun f args =>
match f.constName?, xs.indexOf? x with
| some name, some idx => do
if ←isInductivePredicate name then
if (← isInductivePredicate name) then
let (_, belowTy) ← belowType motive xs idx
let below ← mkFreshExprSyntheticOpaqueMVar belowTy
try
trace[Meta.IndPredBelow.match] "{←Meta.ppGoal below.mvarId!}"
if ←backwardsChaining below.mvarId! 10 then
if (← backwardsChaining below.mvarId! 10) then
trace[Meta.IndPredBelow.match] "Found below term in the local context: {below}"
if ←xs.anyM (isDefEq below) then none else (below, idx.val)
if (← xs.anyM (isDefEq below)) then none else (below, idx.val)
else
trace[Meta.IndPredBelow.match] "could not find below term in the local context"
none
@ -578,7 +579,7 @@ def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat
| _, _ => none
def mkBelow (declName : Name) : MetaM Unit := do
if (←isInductivePredicate declName) then
if (← isInductivePredicate declName) then
let x ← getConstInfoInduct declName
if x.isRec then
let ctx ← IndPredBelow.mkContext declName

10
stage0/src/Lean/MonadEnv.lean generated
View file

@ -19,16 +19,6 @@ def isInductive [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
| some (ConstantInfo.inductInfo ..) => return true
| _ => return false
def isInductivePredicate [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
match (← getEnv).find? declName with
| some (ConstantInfo.inductInfo { type := type, ..}) => return visit type
| _ => return false
where
visit : Expr → Bool
| Expr.sort u .. => u == levelZero
| Expr.forallE _ _ b _ => visit b
| _ => false
def isRecCore (env : Environment) (declName : Name) : Bool :=
match env.find? declName with
| some (ConstantInfo.recInfo ..) => return true

36
stage0/src/bin/lean-gdb.py generated
View file

@ -21,20 +21,20 @@ def unbox(o):
def to_cnstr(o):
return o.cast(gdb.lookup_type('lean_ctor_object').pointer())
def get_tag(header):
return header >> (32 + 8 + 8 + 8)
def get_tag(o):
return o['m_tag']
def get_cnstr_tag(o):
return get_tag(int(o.cast(gdb.lookup_type('lean_ctor_object').pointer()).dereference()['m_header']['m_header']))
return get_tag(o.cast(gdb.lookup_type('lean_object').pointer()))
def get_num_objs(header):
return (header >> (32 + 8 + 8)) & 0xFF
def get_num_objs(o):
return o['m_other']
def get_mem_kind(header):
return (header >> (32 + 8)) & 0xFF
def get_mem_kind(o):
return 0 if o['m_rc'] > 0 else 1 if o['m_rc'] < 0 else 2
def get_rc(header):
return header & 0xFFFFFFFF
def get_rc(o):
return o['m_rc']
char_p = gdb.lookup_type('char').pointer()
@ -45,7 +45,8 @@ def get_closure_arg(o, i):
return o.cast(gdb.lookup_type('lean_closure_object').pointer()).dereference()['m_objs'][i]
def get_c_str(o):
return o.cast(gdb.lookup_type('lean_string_object').pointer()).dereference()['m_data'].reference_value().cast(char_p)
return o.cast(gdb.lookup_type('lean_string_object').pointer()).dereference()['m_data'] \
.cast(gdb.lookup_type('char').pointer()).string()
class LeanObjectPrinter:
"""Print a lean_object object."""
@ -69,17 +70,16 @@ class LeanObjectPrinter:
def __init__(self, val):
self.val = val.address
if not is_scalar(self.val):
self.header = int(self.val.dereference()['m_header'])
self.kind = max(0, get_tag(self.header) - LeanObjectPrinter.lean_max_ctor_tag)
self.kind = max(0, get_tag(self.val) - LeanObjectPrinter.lean_max_ctor_tag)
def to_string(self):
if is_scalar(self.val):
return unbox(self.val)
else:
k = get_mem_kind(self.header)
k = get_mem_kind(self.val)
return "{} ({})".format(LeanObjectPrinter.kinds[self.kind][0],
get_rc(self.header) if k == 0 else
get_rc(self.header) + "/MT" if k == 1 else
get_rc(self.val) if k == 0 else
get_rc(self.val) + "/MT" if k == 1 else
"PERSIST")
def children(self):
@ -92,7 +92,7 @@ class LeanObjectPrinter:
for f in fields:
yield (f, val[f])
if typ == 'ctor':
for i in range(get_num_objs(self.header)):
for i in range(get_num_objs(self.val)):
yield ('', val['m_objs'][i].cast(gdb.lookup_type('lean_object').pointer()))
elif typ == 'array':
for i in range(val['m_size']):
@ -101,7 +101,7 @@ class LeanObjectPrinter:
for i in range(val['m_num_fixed']):
yield ('', val['m_objs'][i].cast(gdb.lookup_type('lean_object').pointer()))
elif typ == 'string':
yield ('', val['m_data'].reference_value().cast(char_p))
yield ('', val['m_data'])
class LeanOptionalPrinter:
@ -135,7 +135,7 @@ class LeanNamePrinter:
def rec(o):
prefix = get_cnstr_obj_arg(o, 0)
part = get_cnstr_obj_arg(o, 1)
s = ("'%s'" % get_c_str(part).string()) if get_cnstr_tag(o) == 1 else str(unbox(part))
s = ("'%s'" % get_c_str(part)) if get_cnstr_tag(o) == 1 else str(unbox(part))
if not is_scalar(prefix):
return "%s.%s" % (rec(prefix), s)
else:

7
stage0/src/kernel/inductive.cpp generated
View file

@ -168,6 +168,7 @@ public:
tc().check(type, m_lparams);
m_nindices.push_back(0);
unsigned i = 0;
type = whnf(type);
while (is_pi(type)) {
if (i < m_nparams) {
if (first) {
@ -181,9 +182,11 @@ public:
}
i++;
} else {
type = binding_body(type);
expr local = mk_local_decl_for(type);
type = instantiate(binding_body(type), local);
m_nindices.back()++;
}
type = whnf(type);
}
if (i != m_nparams)
throw kernel_exception(m_env, "number of parameters mismatch in inductive datatype declaration");
@ -527,6 +530,7 @@ public:
rec_info info;
expr t = ind_type.get_type();
unsigned i = 0;
t = whnf(t);
while (is_pi(t)) {
if (i < m_nparams) {
t = instantiate(binding_body(t), m_params[i]);
@ -536,6 +540,7 @@ public:
t = instantiate(binding_body(t), idx);
}
i++;
t = whnf(t);
}
info.m_major = mk_local_decl("t", mk_app(mk_app(m_ind_cnsts[d_idx], m_params), info.m_indices));
expr C_ty = mk_sort(m_elim_level);

4
stage0/src/library/constructions/brec_on.cpp generated
View file

@ -64,7 +64,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
ref_type = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_level_zero());
} else if (is_reflexive) {
blvls = lps;
rlvl = get_datatype_level(ind_info.get_type());
rlvl = get_datatype_level(env, ind_info.get_type());
// if rlvl is of the form (max 1 l), then rlvl <- l
if (is_max(rlvl) && is_one(max_lhs(rlvl)))
rlvl = max_rhs(rlvl);
@ -205,7 +205,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
} else if (is_reflexive) {
blps = lps;
blvls = cons(lvl, lvls);
rlvl = get_datatype_level(ind_info.get_type());
rlvl = get_datatype_level(env, ind_info.get_type());
// if rlvl is of the form (max 1 l), then rlvl <- l
if (is_max(rlvl) && is_one(max_lhs(rlvl)))
rlvl = max_rhs(rlvl);

3
stage0/src/library/constructions/no_confusion.cpp generated
View file

@ -40,6 +40,7 @@ static optional<environment> mk_no_confusion_type(environment const & env, name
/* All inductive datatype parameters and indices are arguments */
buffer<expr> args;
ind_type = to_telescope(lctx, ngen, ind_type, args, some(mk_implicit_binder_info()));
ind_type = type_checker(env, lctx).whnf(ind_type);
if (!is_sort(ind_type) || args.size() < nparams)
throw_corrupted(n);
level ind_lvl = sort_level(ind_type);
@ -142,7 +143,7 @@ environment mk_no_confusion(environment const & env, name const & n) {
names lps = no_confusion_type_info.get_lparams();
levels ls = lparams_to_levels(lps);
expr ind_type = instantiate_type_lparams(ind_info, tail(ls));
level ind_lvl = get_datatype_level(ind_type);
level ind_lvl = get_datatype_level(env, ind_type);
expr no_confusion_type_type = instantiate_type_lparams(no_confusion_type_info, ls);
buffer<expr> args;
expr type = no_confusion_type_type;

18
stage0/src/library/util.cpp generated
View file

@ -191,10 +191,16 @@ bool is_recursive_datatype(environment const & env, name const & n) {
return info.is_inductive() && info.to_inductive_val().is_rec();
}
level get_datatype_level(expr const & ind_type) {
expr it = ind_type;
while (is_pi(it))
it = binding_body(it);
static name * g_util_fresh = nullptr;
level get_datatype_level(environment const & env, expr const & ind_type) {
local_ctx lctx;
name_generator ngen(*g_util_fresh);
expr it = type_checker(env, lctx).whnf(ind_type);
while (is_pi(it)) {
expr local = lctx.mk_local_decl(ngen, binding_name(it), binding_domain(it), binding_info(it));
it = type_checker(env, lctx).whnf(instantiate(binding_body(it), local));
}
if (is_sort(it)) {
return sort_level(it);
} else {
@ -216,7 +222,7 @@ bool is_inductive_predicate(environment const & env, name const & n) {
constant_info info = env.get(n);
if (!info.is_inductive())
return false;
return is_zero(get_datatype_level(env.get(n).get_type()));
return is_zero(get_datatype_level(env, env.get(n).get_type()));
}
bool can_elim_to_type(environment const & env, name const & n) {
@ -257,8 +263,6 @@ optional<name> is_constructor_app_ext(environment const & env, expr const & e) {
return is_constructor_app_ext(env, *it);
}
static name * g_util_fresh = nullptr;
void get_constructor_relevant_fields(environment const & env, name const & n, buffer<bool> & result) {
constant_info info = env.get(n);
lean_assert(info.is_constructor());

2
stage0/src/library/util.h generated
View file

@ -126,7 +126,7 @@ name get_constructor_inductive_type(environment const & env, name const & ctor_n
/** \brief Return the universe where inductive datatype resides
\pre \c ind_type is of the form <tt>Pi (a_1 : A_1) (a_2 : A_2[a_1]) ..., Type.{lvl}</tt> */
level get_datatype_level(expr const & ind_type);
level get_datatype_level(environment const & env, expr const & ind_type);
/** \brief "Consume" Pi-type `type`. This procedure creates free variables based on the domain of `type` using `lctx`,
and store them in telescope and updates . If `binfo` is provided, then the free variables are annotated with

2
stage0/src/runtime/CMakeLists.txt generated
View file

@ -2,7 +2,7 @@ set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp mpq.cpp utf8.cpp
object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
stackinfo.cpp compact.cpp init_module.cpp io.cpp hash.cpp
platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
process.cpp object_ref.cpp)
process.cpp object_ref.cpp mpn.cpp)
add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
set_target_properties(leanrt_initial-exec PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})

356
stage0/src/runtime/mpn.cpp generated Normal file
View file

@ -0,0 +1,356 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
mpn.cpp
Abstract:
Multi Precision Natural Numbers
Author:
Christoph Wintersteiger (cwinter) 2011-11-16.
Revision History:
--*/
#include <stdint.h>
#include "runtime/mpn.h"
#include "runtime/debug.h"
#include "runtime/buffer.h"
#define max(a,b) (((a) > (b)) ? (a) : (b))
namespace lean {
typedef uint64_t mpn_double_digit;
static_assert(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit), "size alignment");
static const mpn_digit zero = 0;
int mpn_compare(mpn_digit const * a, size_t const lnga,
mpn_digit const * b, size_t const lngb) {
int res = 0;
size_t j = max(lnga, lngb) - 1;
for (; j != (size_t)-1 && res == 0; j--) {
mpn_digit const & u_j = (j < lnga) ? a[j] : zero;
mpn_digit const & v_j = (j < lngb) ? b[j] : zero;
if (u_j > v_j)
res = 1;
else if (u_j < v_j)
res = -1;
}
return res;
}
void mpn_add(mpn_digit const * a, size_t const lnga,
mpn_digit const * b, size_t const lngb,
mpn_digit * c, size_t const lngc_alloc,
size_t * plngc) {
// Essentially Knuth's Algorithm A
size_t len = max(lnga, lngb);
lean_assert(lngc_alloc == len+1 && len > 0);
mpn_digit k = 0;
mpn_digit r;
bool c1, c2;
for (size_t j = 0; j < len; j++) {
mpn_digit const & u_j = (j < lnga) ? a[j] : zero;
mpn_digit const & v_j = (j < lngb) ? b[j] : zero;
r = u_j + v_j; c1 = r < u_j;
c[j] = r + k; c2 = c[j] < r;
k = c1 | c2;
}
c[len] = k;
size_t &os = *plngc;
for (os = len+1; os > 1 && c[os-1] == 0; ) os--;
lean_assert(os > 0 && os <= len+1);
}
void mpn_sub(mpn_digit const * a, size_t const lnga,
mpn_digit const * b, size_t const lngb,
mpn_digit * c, mpn_digit * pborrow) {
// Essentially Knuth's Algorithm S
size_t len = max(lnga, lngb);
mpn_digit & k = *pborrow; k = 0;
mpn_digit r;
bool c1, c2;
for (size_t j = 0; j < len; j++) {
mpn_digit const & u_j = (j < lnga) ? a[j] : zero;
mpn_digit const & v_j = (j < lngb) ? b[j] : zero;
r = u_j - v_j; c1 = r > u_j;
c[j] = r - k; c2 = c[j] > r;
k = c1 | c2;
}
}
void mpn_mul(mpn_digit const * a, size_t const lnga,
mpn_digit const * b, size_t const lngb,
mpn_digit * c) {
// Essentially Knuth's Algorithm M.
// Perhaps implement a more efficient version, see e.g., Knuth, Section 4.3.3.
size_t i;
mpn_digit k;
#define DIGIT_BITS (sizeof(mpn_digit)*8)
#define HALF_BITS (sizeof(mpn_digit)*4)
for (unsigned i = 0; i < lnga; i++)
c[i] = 0;
for (size_t j = 0; j < lngb; j++) {
mpn_digit const & v_j = b[j];
if (v_j == 0) { // This branch may be omitted according to Knuth.
c[j+lnga] = 0;
}
else {
k = 0;
for (i = 0; i < lnga; i++) {
mpn_digit const & u_i = a[i];
mpn_double_digit t;
t = ((mpn_double_digit)u_i * (mpn_double_digit)v_j) +
(mpn_double_digit) c[i+j] +
(mpn_double_digit) k;
c[i+j] = (t << DIGIT_BITS) >> DIGIT_BITS;
k = t >> DIGIT_BITS;
}
c[j+lnga] = k;
}
}
}
#define MASK_FIRST (~((mpn_digit)(-1) >> 1))
#define FIRST_BITS(N, X) ((X) >> (DIGIT_BITS-(N)))
#define LAST_BITS(N, X) (((X) << (DIGIT_BITS-(N))) >> (DIGIT_BITS-(N)))
#define BASE ((mpn_double_digit)0x01 << DIGIT_BITS)
class mpn_buffer : public buffer<mpn_digit> {
public:
mpn_buffer() : buffer<mpn_digit>() {}
mpn_buffer(size_t nsz, const mpn_digit & elem = 0):buffer<mpn_digit>() {
for (size_t i = 0; i < nsz; i++) push_back(elem);
}
void resize(size_t nsz, const mpn_digit & elem = 0) {
buffer<mpn_digit>::resize(static_cast<unsigned>(nsz), elem);
}
mpn_digit & operator[](size_t idx) {
return buffer<mpn_digit>::operator[](static_cast<unsigned>(idx));
}
const mpn_digit & operator[](size_t idx) const {
return buffer<mpn_digit>::operator[](static_cast<unsigned>(idx));
}
};
static size_t div_normalize(mpn_digit const * numer, size_t const lnum,
mpn_digit const * denom, size_t const lden,
mpn_buffer & n_numer,
mpn_buffer & n_denom) {
size_t d = 0;
while (lden > 0 && ((denom[lden-1] << d) & MASK_FIRST) == 0) d++;
lean_assert(d < DIGIT_BITS);
n_numer.resize(lnum+1);
n_denom.resize(lden);
if (d == 0) {
n_numer[lnum] = 0;
for (size_t i = 0; i < lnum; i++)
n_numer[i] = numer[i];
for (size_t i = 0; i < lden; i++)
n_denom[i] = denom[i];
}
else if (lnum != 0) {
lean_assert(lden > 0);
mpn_digit q = FIRST_BITS(d, numer[lnum-1]);
n_numer[lnum] = q;
for (size_t i = lnum-1; i > 0; i--)
n_numer[i] = (numer[i] << d) | FIRST_BITS(d, numer[i-1]);
n_numer[0] = numer[0] << d;
for (size_t i = lden-1; i > 0; i--)
n_denom[i] = denom[i] << d | FIRST_BITS(d, denom[i-1]);
n_denom[0] = denom[0] << d;
}
else {
d = 0;
}
return d;
}
static void div_unnormalize(mpn_buffer & numer, mpn_buffer & denom,
size_t const d, mpn_digit * rem) {
if (d == 0) {
for (size_t i = 0; i < denom.size(); i++)
rem[i] = numer[i];
}
else {
for (size_t i = 0; i < denom.size()-1; i++)
rem[i] = numer[i] >> d | (LAST_BITS(d, numer[i+1]) << (DIGIT_BITS-d));
rem[denom.size()-1] = numer[denom.size()-1] >> d;
}
}
static void div_1(mpn_buffer & numer, mpn_digit const denom,
mpn_digit * quot) {
mpn_double_digit q_hat, temp, ms;
mpn_digit borrow;
for (size_t j = numer.size()-1; j > 0; j--) {
temp = (((mpn_double_digit)numer[j]) << DIGIT_BITS) | ((mpn_double_digit)numer[j-1]);
q_hat = temp / (mpn_double_digit) denom;
if (q_hat >= BASE) {
lean_unreachable(); // is this reachable with normalized v?
}
lean_assert(q_hat < BASE);
ms = temp - (q_hat * (mpn_double_digit) denom);
borrow = ms > temp;
numer[j-1] = (mpn_digit) ms;
numer[j] = ms >> DIGIT_BITS;
quot[j-1] = (mpn_digit) q_hat;
if (borrow) {
quot[j-1]--;
numer[j] = numer[j-1] + denom;
}
}
}
static void div_n(mpn_buffer & numer, mpn_buffer const & denom,
mpn_digit * quot, mpn_digit * rem,
mpn_buffer & ms, mpn_buffer & ab) {
lean_assert(denom.size() > 1);
// This is essentially Knuth's Algorithm D.
size_t m = numer.size() - denom.size();
size_t n = denom.size();
lean_assert(numer.size() == m+n);
ms.resize(n+1);
mpn_double_digit q_hat, temp, r_hat;
mpn_digit borrow;
for (size_t j = m-1; j != (size_t)-1; j--) {
temp = (((mpn_double_digit)numer[j+n]) << DIGIT_BITS) | ((mpn_double_digit)numer[j+n-1]);
q_hat = temp / (mpn_double_digit) denom[n-1];
r_hat = temp % (mpn_double_digit) denom[n-1];
recheck:
if (q_hat >= BASE ||
((q_hat * denom[n-2]) > ((r_hat << DIGIT_BITS) + numer[j+n-2]))) {
q_hat--;
r_hat += denom[n-1];
if (r_hat < BASE) goto recheck;
}
lean_assert(q_hat < BASE);
// Replace numer[j+n]...numer[j] with
// numer[j+n]...numer[j] - q * (denom[n-1]...denom[0])
mpn_digit q_hat_small = (mpn_digit)q_hat;
mpn_mul(&q_hat_small, 1, denom.data(), n, ms.data());
mpn_sub(&numer[j], n+1, ms.data(), n+1, &numer[j], &borrow);
quot[j] = q_hat_small;
if (borrow) {
quot[j]--;
ab.resize(n+2);
size_t real_size;
mpn_add(denom.data(), n, &numer[j], n+1, ab.data(), n+2, &real_size);
for (size_t i = 0; i < n+1; i++)
numer[j+i] = ab[i];
}
}
}
void mpn_div(mpn_digit const * numer, size_t const lnum,
mpn_digit const * denom, size_t const lden,
mpn_digit * quot,
mpn_digit * rem) {
if (lnum < lden) {
for (size_t i = 0; i < (lnum-lden+1); i++)
quot[i] = 0;
for (size_t i = 0; i < lden; i++)
rem[i] = (i < lnum) ? numer[i] : 0;
return;
}
bool all_zero = true;
for (size_t i = 0; i < lden && all_zero; i++)
if (denom[i] != zero) all_zero = false;
lean_assert(!all_zero);
lean_assert(denom[lden-1] != 0);
if (lnum == 1 && lden == 1) {
*quot = numer[0] / denom[0];
*rem = numer[0] % denom[0];
}
else if (lnum < lden || (lnum == lden && numer[lnum-1] < denom[lden-1])) {
*quot = 0;
for (size_t i = 0; i < lden; i++)
rem[i] = (i < lnum) ? numer[i] : 0;
}
else {
mpn_buffer u, v, t_ms, t_ab;
size_t d = div_normalize(numer, lnum, denom, lden, u, v);
if (lden == 1)
div_1(u, v[0], quot);
else
div_n(u, v, quot, rem, t_ms, t_ab);
div_unnormalize(u, v, d, rem);
}
#ifdef LEAN_DEBUG
mpn_buffer temp(lnum+1, 0);
mpn_mul(quot, lnum-lden+1, denom, lden, temp.data());
size_t real_size;
mpn_add(temp.data(), lnum, rem, lden, temp.data(), lnum+1, &real_size);
bool ok = true;
for (size_t i = 0; i < lnum && ok; i++)
if (temp[i] != numer[i]) ok = false;
if (temp[lnum] != 0) ok = false;
lean_assert(ok);
#endif
}
char * mpn_to_string(mpn_digit const * a, size_t const lng, char * buf, size_t const lbuf) {
lean_assert(buf && lbuf > 0);
if (lng == 1) {
#ifdef _WINDOWS
sprintf_s(buf, lbuf, "%u", *a);
#else
snprintf(buf, lbuf, "%u", *a);
#endif
}
else {
mpn_buffer temp(lng, 0), t_numer(lng+1, 0), t_denom(1, 0);
for (unsigned i = 0; i < lng; i++)
temp[i] = a[i];
size_t j = 0;
mpn_digit rem;
mpn_digit ten = 10;
while (!temp.empty() && (temp.size() > 1 || temp[0] != 0)) {
size_t d = div_normalize(&temp[0], temp.size(), &ten, 1, t_numer, t_denom);
div_1(t_numer, t_denom[0], &temp[0]);
div_unnormalize(t_numer, t_denom, d, &rem);
buf[j++] = '0' + rem;
while (!temp.empty() && temp.back() == 0)
temp.pop_back();
}
buf[j] = 0;
j--;
size_t mid = (j/2) + ((j % 2) ? 1 : 0);
for (size_t i = 0; i < mid; i++)
std::swap(buf[i], buf[j-i]);
}
return buf;
}
}

48
stage0/src/runtime/mpn.h generated Normal file
View file

@ -0,0 +1,48 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
mpn.h
Abstract:
Multi Precision Natural Numbers
Author:
Christoph Wintersteiger (cwinter) 2011-11-16.
Revision History:
--*/
#pragma once
#include <stddef.h>
namespace lean {
typedef unsigned int mpn_digit;
int mpn_compare(mpn_digit const * a, size_t lnga,
mpn_digit const * b, size_t lngb);
void mpn_add(mpn_digit const * a, size_t lnga,
mpn_digit const * b, size_t lngb,
mpn_digit *c, size_t lngc_alloc,
size_t * plngc);
void mpn_sub(mpn_digit const * a, size_t lnga,
mpn_digit const * b, size_t lngb,
mpn_digit * c, mpn_digit * pborrow);
void mpn_mul(mpn_digit const * a, size_t lnga,
mpn_digit const * b, size_t lngb,
mpn_digit * c);
void mpn_div(mpn_digit const * numer, size_t lnum,
mpn_digit const * denom, size_t lden,
mpn_digit * quot,
mpn_digit * rem);
char * mpn_to_string(mpn_digit const * a, size_t lng,
char * buf, size_t lbuf);
}

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

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Elab
// Imports: Init Lean.Elab.Import Lean.Elab.Exception Lean.Elab.Command Lean.Elab.Term Lean.Elab.App Lean.Elab.Binders Lean.Elab.LetRec Lean.Elab.Frontend Lean.Elab.BuiltinNotation Lean.Elab.Declaration Lean.Elab.Tactic Lean.Elab.Match Lean.Elab.Quotation Lean.Elab.Syntax Lean.Elab.Do Lean.Elab.StructInst Lean.Elab.Inductive Lean.Elab.Structure Lean.Elab.Print Lean.Elab.MutualDef Lean.Elab.PreDefinition Lean.Elab.Deriving Lean.Elab.DeclarationRange Lean.Elab.Extra Lean.Elab.GenInjective Lean.Elab.BuiltinTerm Lean.Elab.Arg Lean.Elab.PatternVar Lean.Elab.ElabRules Lean.Elab.Macro Lean.Elab.Notation Lean.Elab.Mixfix Lean.Elab.MacroRules Lean.Elab.BuiltinCommand
// Imports: Init Lean.Elab.Import Lean.Elab.Exception Lean.Elab.Command Lean.Elab.Term Lean.Elab.App Lean.Elab.Binders Lean.Elab.LetRec Lean.Elab.Frontend Lean.Elab.BuiltinNotation Lean.Elab.Declaration Lean.Elab.Tactic Lean.Elab.Match Lean.Elab.Quotation Lean.Elab.Syntax Lean.Elab.Do Lean.Elab.StructInst Lean.Elab.Inductive Lean.Elab.Structure Lean.Elab.Print Lean.Elab.MutualDef Lean.Elab.AuxDef Lean.Elab.PreDefinition Lean.Elab.Deriving Lean.Elab.DeclarationRange Lean.Elab.Extra Lean.Elab.GenInjective Lean.Elab.BuiltinTerm Lean.Elab.Arg Lean.Elab.PatternVar Lean.Elab.ElabRules Lean.Elab.Macro Lean.Elab.Notation Lean.Elab.Mixfix Lean.Elab.MacroRules Lean.Elab.BuiltinCommand
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -34,6 +34,7 @@ lean_object* initialize_Lean_Elab_Inductive(lean_object*);
lean_object* initialize_Lean_Elab_Structure(lean_object*);
lean_object* initialize_Lean_Elab_Print(lean_object*);
lean_object* initialize_Lean_Elab_MutualDef(lean_object*);
lean_object* initialize_Lean_Elab_AuxDef(lean_object*);
lean_object* initialize_Lean_Elab_PreDefinition(lean_object*);
lean_object* initialize_Lean_Elab_Deriving(lean_object*);
lean_object* initialize_Lean_Elab_DeclarationRange(lean_object*);
@ -116,6 +117,9 @@ lean_dec_ref(res);
res = initialize_Lean_Elab_MutualDef(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_AuxDef(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_PreDefinition(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

1817
stage0/stdlib/Lean/Elab/AuxDef.c generated Normal file
View file

File diff suppressed because it is too large Load diff

5438
stage0/stdlib/Lean/Elab/ElabRules.c generated
View file

File diff suppressed because it is too large Load diff

976
stage0/stdlib/Lean/Elab/Inductive.c generated
View file

File diff suppressed because it is too large Load diff

2868
stage0/stdlib/Lean/Elab/MacroRules.c generated
View file

File diff suppressed because it is too large Load diff

10485
stage0/stdlib/Lean/Elab/Notation.c generated
View file

File diff suppressed because it is too large Load diff

923
stage0/stdlib/Lean/Elab/PreDefinition/Structural/FindRecArg.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -22,6 +22,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_resettingSynthInstanceCacheWhen___rarg___bo
lean_object* lean_array_set(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Meta_mkFreshExprMVarAt___spec__2(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarAtCore___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*);
static lean_object* l_Lean_Meta_isInductivePredicate___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_instMonadMetaM___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_usize_add(size_t, size_t);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withNewMCtxDepthImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -254,6 +255,7 @@ static lean_object* l_Lean_Meta_instAlternativeMetaM___closed__1;
LEAN_EXPORT lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_LocalContext_setBinderInfo(lean_object*, lean_object*, uint8_t);
static lean_object* l_Lean_Meta_throwUnknownFVar___rarg___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_isInductivePredicate(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_getConfig___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassQuickConst_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_throwUnknownFVar___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -492,6 +494,7 @@ uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallBoundedTelescopeImp(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_SavedState_restore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_instMetaEvalMetaM___rarg___closed__6;
LEAN_EXPORT lean_object* l_Lean_Meta_isInductivePredicate___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withLocalDecl___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_lambdaMetaTelescope_process___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -511,6 +514,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_synthPending___boxed(lean_object*, lean_obj
LEAN_EXPORT uint8_t l_Lean_Meta_ParamInfo_isExplicit(lean_object*);
lean_object* lean_expr_update_proj(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_instInhabitedCache___closed__2;
LEAN_EXPORT lean_object* l_Lean_Meta_isInductivePredicate___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLocalDeclImp(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_instInhabitedParamInfo;
LEAN_EXPORT lean_object* l_Lean_Meta_lambdaLetTelescope(lean_object*);
@ -771,6 +775,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_mapError___rarg(lean_object*, lean_object*,
LEAN_EXPORT lean_object* l_Lean_Meta_getPostponed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_getParamNames(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withNewFVar(lean_object*);
uint8_t lean_level_eq(lean_object*, lean_object*);
uint32_t lean_uint32_of_nat(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_setMCtx(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_getLocalDeclFromUserName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -28958,6 +28963,257 @@ lean_dec(x_3);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_isInductivePredicate___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) {
_start:
{
lean_object* x_8;
x_8 = l_Lean_Meta_whnfD(x_2, x_3, x_4, x_5, x_6, x_7);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9;
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
if (lean_obj_tag(x_9) == 3)
{
uint8_t x_10;
x_10 = !lean_is_exclusive(x_8);
if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; lean_object* x_15;
x_11 = lean_ctor_get(x_8, 0);
lean_dec(x_11);
x_12 = lean_ctor_get(x_9, 0);
lean_inc(x_12);
lean_dec(x_9);
x_13 = l_Lean_levelZero;
x_14 = lean_level_eq(x_12, x_13);
lean_dec(x_12);
x_15 = lean_box(x_14);
lean_ctor_set(x_8, 0, x_15);
return x_8;
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; uint8_t x_19; lean_object* x_20; lean_object* x_21;
x_16 = lean_ctor_get(x_8, 1);
lean_inc(x_16);
lean_dec(x_8);
x_17 = lean_ctor_get(x_9, 0);
lean_inc(x_17);
lean_dec(x_9);
x_18 = l_Lean_levelZero;
x_19 = lean_level_eq(x_17, x_18);
lean_dec(x_17);
x_20 = lean_box(x_19);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_16);
return x_21;
}
}
else
{
uint8_t x_22;
lean_dec(x_9);
x_22 = !lean_is_exclusive(x_8);
if (x_22 == 0)
{
lean_object* x_23; uint8_t x_24; lean_object* x_25;
x_23 = lean_ctor_get(x_8, 0);
lean_dec(x_23);
x_24 = 0;
x_25 = lean_box(x_24);
lean_ctor_set(x_8, 0, x_25);
return x_8;
}
else
{
lean_object* x_26; uint8_t x_27; lean_object* x_28; lean_object* x_29;
x_26 = lean_ctor_get(x_8, 1);
lean_inc(x_26);
lean_dec(x_8);
x_27 = 0;
x_28 = lean_box(x_27);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_26);
return x_29;
}
}
}
else
{
uint8_t x_30;
x_30 = !lean_is_exclusive(x_8);
if (x_30 == 0)
{
return x_8;
}
else
{
lean_object* x_31; lean_object* x_32; lean_object* x_33;
x_31 = lean_ctor_get(x_8, 0);
x_32 = lean_ctor_get(x_8, 1);
lean_inc(x_32);
lean_inc(x_31);
lean_dec(x_8);
x_33 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_33, 0, x_31);
lean_ctor_set(x_33, 1, x_32);
return x_33;
}
}
}
}
static lean_object* _init_l_Lean_Meta_isInductivePredicate___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Meta_isInductivePredicate___lambda__1___boxed), 7, 0);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_isInductivePredicate(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; uint8_t x_8;
x_7 = lean_st_ref_get(x_5, x_6);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_7, 0);
x_10 = lean_ctor_get(x_7, 1);
x_11 = lean_ctor_get(x_9, 0);
lean_inc(x_11);
lean_dec(x_9);
x_12 = lean_environment_find(x_11, x_1);
if (lean_obj_tag(x_12) == 0)
{
uint8_t x_13; lean_object* x_14;
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_13 = 0;
x_14 = lean_box(x_13);
lean_ctor_set(x_7, 0, x_14);
return x_7;
}
else
{
lean_object* x_15;
x_15 = lean_ctor_get(x_12, 0);
lean_inc(x_15);
lean_dec(x_12);
if (lean_obj_tag(x_15) == 5)
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_free_object(x_7);
x_16 = lean_ctor_get(x_15, 0);
lean_inc(x_16);
lean_dec(x_15);
x_17 = lean_ctor_get(x_16, 0);
lean_inc(x_17);
lean_dec(x_16);
x_18 = lean_ctor_get(x_17, 2);
lean_inc(x_18);
lean_dec(x_17);
x_19 = l_Lean_Meta_isInductivePredicate___closed__1;
x_20 = l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_getParamNames___spec__2___rarg(x_18, x_19, x_2, x_3, x_4, x_5, x_10);
return x_20;
}
else
{
uint8_t x_21; lean_object* x_22;
lean_dec(x_15);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_21 = 0;
x_22 = lean_box(x_21);
lean_ctor_set(x_7, 0, x_22);
return x_7;
}
}
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_23 = lean_ctor_get(x_7, 0);
x_24 = lean_ctor_get(x_7, 1);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_7);
x_25 = lean_ctor_get(x_23, 0);
lean_inc(x_25);
lean_dec(x_23);
x_26 = lean_environment_find(x_25, x_1);
if (lean_obj_tag(x_26) == 0)
{
uint8_t x_27; lean_object* x_28; lean_object* x_29;
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_27 = 0;
x_28 = lean_box(x_27);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_24);
return x_29;
}
else
{
lean_object* x_30;
x_30 = lean_ctor_get(x_26, 0);
lean_inc(x_30);
lean_dec(x_26);
if (lean_obj_tag(x_30) == 5)
{
lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_31 = lean_ctor_get(x_30, 0);
lean_inc(x_31);
lean_dec(x_30);
x_32 = lean_ctor_get(x_31, 0);
lean_inc(x_32);
lean_dec(x_31);
x_33 = lean_ctor_get(x_32, 2);
lean_inc(x_33);
lean_dec(x_32);
x_34 = l_Lean_Meta_isInductivePredicate___closed__1;
x_35 = l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_getParamNames___spec__2___rarg(x_33, x_34, x_2, x_3, x_4, x_5, x_24);
return x_35;
}
else
{
uint8_t x_36; lean_object* x_37; lean_object* x_38;
lean_dec(x_30);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_36 = 0;
x_37 = lean_box(x_36);
x_38 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_38, 0, x_37);
lean_ctor_set(x_38, 1, x_24);
return x_38;
}
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_isInductivePredicate___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) {
_start:
{
lean_object* x_8;
x_8 = l_Lean_Meta_isInductivePredicate___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_1);
return x_8;
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Data_LOption(lean_object*);
lean_object* initialize_Lean_Environment(lean_object*);
@ -29323,6 +29579,8 @@ l_Lean_Meta_instAlternativeMetaM___closed__3 = _init_l_Lean_Meta_instAlternative
lean_mark_persistent(l_Lean_Meta_instAlternativeMetaM___closed__3);
l_Lean_Meta_instAlternativeMetaM = _init_l_Lean_Meta_instAlternativeMetaM();
lean_mark_persistent(l_Lean_Meta_instAlternativeMetaM);
l_Lean_Meta_isInductivePredicate___closed__1 = _init_l_Lean_Meta_isInductivePredicate___closed__1();
lean_mark_persistent(l_Lean_Meta_isInductivePredicate___closed__1);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

5898
stage0/stdlib/Lean/Meta/IndPredBelow.c generated
View file

File diff suppressed because it is too large Load diff

230
stage0/stdlib/Lean/Meta/Injective.c generated
View file

@ -33,7 +33,6 @@ lean_object* l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_getParamNames___
LEAN_EXPORT lean_object* l_Lean_Meta_elimOptParam___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_injTheoremFailureHeader___closed__3;
static lean_object* l_Subarray_forInUnsafe_loop___at___private_Lean_Meta_Injective_0__Lean_Meta_mkAnd_x3f___spec__1___closed__1;
lean_object* lean_environment_find(lean_object*, lean_object*);
lean_object* l_Lean_getConstInfo___at_Lean_Meta_mkConstWithFreshMVarLevels___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_elimOptParam___lambda__1___closed__2;
LEAN_EXPORT lean_object* l_Subarray_forInUnsafe_loop___at___private_Lean_Meta_Injective_0__Lean_Meta_mkAnd_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -48,7 +47,6 @@ lean_object* l_Array_toSubarray___rarg(lean_object*, lean_object*, lean_object*)
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremValue___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_mkInjectiveTheorems___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_casesAnd(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1681____closed__2;
static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_injTheoremFailureHeader___closed__1;
@ -71,6 +69,7 @@ lean_object* l_Lean_Meta_apply(lean_object*, lean_object*, lean_object*, lean_ob
LEAN_EXPORT lean_object* l_Lean_Meta_elimOptParam___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
static lean_object* l_Subarray_forInUnsafe_loop___at___private_Lean_Meta_Injective_0__Lean_Meta_mkAnd_x3f___spec__1___closed__2;
lean_object* l_Lean_Meta_isInductivePredicate(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Meta_Injective_0__Lean_Meta_throwInjectiveTheoremFailure___spec__1(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_intro1Core(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -84,15 +83,17 @@ static lean_object* l_Lean_Meta_mkInjectiveTheoremNameFor___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_mkInjectiveEqTheoremNameFor(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_mkInjectiveEqTheoremNameFor___boxed(lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
static lean_object* l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1___closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkAnd_x3f(lean_object*);
extern lean_object* l_Lean_Meta_simpExtension;
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Injective___hyg_1681____closed__3;
lean_object* l_Lean_Option_register___at_Std_Format_initFn____x40_Lean_Data_Format___hyg_54____spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_mkInjectiveTheorems___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1___closed__1;
lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f_mkArgs2(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*);
static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTheoremValue___lambda__1___closed__3;
LEAN_EXPORT lean_object* l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTheoremValue___lambda__1___closed__5;
static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f_mkArgs2___closed__3;
static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTheoremValue___lambda__1___closed__6;
@ -108,8 +109,6 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Meta_Injective_0_
LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f___lambda__3(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isAppOfArity(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_isInductivePredicate_visit(lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkInjectiveTheorems___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_reverse___rarg(lean_object*);
uint8_t l_Array_isEmpty___rarg(lean_object*);
@ -120,19 +119,18 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_injTheorem
lean_object* lean_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_throwInjectiveTheoremFailure(lean_object*);
lean_object* l_Lean_Meta_saturate(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2___closed__1;
size_t lean_usize_of_nat(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f___spec__2(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_mkInjectiveTheorems___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTheoremValue(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withNewBinderInfos___at___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2___closed__2;
LEAN_EXPORT lean_object* l_Subarray_forInUnsafe_loop___at___private_Lean_Meta_Injective_0__Lean_Meta_mkAnd_x3f___spec__1(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Meta_forallTelescope___at___private_Lean_Meta_InferType_0__Lean_Meta_inferForallType___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTheoremValue___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_mkInjectiveTheoremNameFor(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkInjectiveTheorems___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_substEqs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
lean_object* l_Lean_Meta_assumptionCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -144,7 +142,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_mkInjectiveTheoremNameFor___boxed(lean_obje
LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheorem(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveEqTheoremValue___lambda__1___closed__7;
lean_object* l_Lean_Name_append(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Meta_addPPExplicitToExposeDiff_visit___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_mapTRAux___at_Lean_mkConstWithLevelParams___spec__1(lean_object*, lean_object*);
@ -160,6 +157,7 @@ lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_objec
static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_solveEqOfCtorEq___closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_indentD(lean_object*);
LEAN_EXPORT lean_object* l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_genInjectivity;
static lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f_mkArgs2___closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f_mkArgs2___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*);
@ -173,12 +171,11 @@ lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_elimOptParam___closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremType_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_occurs(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_isInductivePredicate___at_Lean_Meta_mkInjectiveTheorems___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addDecl___at_Lean_Meta_mkAuxLemma___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_isInductivePredicate___at_Lean_Meta_mkInjectiveTheorems___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkAppB(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isProp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_mkInjectiveTheorems___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_panic___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_solveSelfMax___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x3f___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*);
@ -4749,127 +4746,7 @@ lean_ctor_set(x_4, 1, x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_isInductivePredicate___at_Lean_Meta_mkInjectiveTheorems___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; uint8_t x_8;
x_7 = lean_st_ref_get(x_5, x_6);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = lean_ctor_get(x_7, 0);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
lean_dec(x_9);
x_11 = lean_environment_find(x_10, x_1);
if (lean_obj_tag(x_11) == 0)
{
uint8_t x_12; lean_object* x_13;
x_12 = 0;
x_13 = lean_box(x_12);
lean_ctor_set(x_7, 0, x_13);
return x_7;
}
else
{
lean_object* x_14;
x_14 = lean_ctor_get(x_11, 0);
lean_inc(x_14);
lean_dec(x_11);
if (lean_obj_tag(x_14) == 5)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19;
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
lean_dec(x_14);
x_16 = lean_ctor_get(x_15, 0);
lean_inc(x_16);
lean_dec(x_15);
x_17 = lean_ctor_get(x_16, 2);
lean_inc(x_17);
lean_dec(x_16);
x_18 = l_Lean_isInductivePredicate_visit(x_17);
lean_dec(x_17);
x_19 = lean_box(x_18);
lean_ctor_set(x_7, 0, x_19);
return x_7;
}
else
{
uint8_t x_20; lean_object* x_21;
lean_dec(x_14);
x_20 = 0;
x_21 = lean_box(x_20);
lean_ctor_set(x_7, 0, x_21);
return x_7;
}
}
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_22 = lean_ctor_get(x_7, 0);
x_23 = lean_ctor_get(x_7, 1);
lean_inc(x_23);
lean_inc(x_22);
lean_dec(x_7);
x_24 = lean_ctor_get(x_22, 0);
lean_inc(x_24);
lean_dec(x_22);
x_25 = lean_environment_find(x_24, x_1);
if (lean_obj_tag(x_25) == 0)
{
uint8_t x_26; lean_object* x_27; lean_object* x_28;
x_26 = 0;
x_27 = lean_box(x_26);
x_28 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_28, 0, x_27);
lean_ctor_set(x_28, 1, x_23);
return x_28;
}
else
{
lean_object* x_29;
x_29 = lean_ctor_get(x_25, 0);
lean_inc(x_29);
lean_dec(x_25);
if (lean_obj_tag(x_29) == 5)
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33; lean_object* x_34; lean_object* x_35;
x_30 = lean_ctor_get(x_29, 0);
lean_inc(x_30);
lean_dec(x_29);
x_31 = lean_ctor_get(x_30, 0);
lean_inc(x_31);
lean_dec(x_30);
x_32 = lean_ctor_get(x_31, 2);
lean_inc(x_32);
lean_dec(x_31);
x_33 = l_Lean_isInductivePredicate_visit(x_32);
lean_dec(x_32);
x_34 = lean_box(x_33);
x_35 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_35, 0, x_34);
lean_ctor_set(x_35, 1, x_23);
return x_35;
}
else
{
uint8_t x_36; lean_object* x_37; lean_object* x_38;
lean_dec(x_29);
x_36 = 0;
x_37 = lean_box(x_36);
x_38 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_38, 0, x_37);
lean_ctor_set(x_38, 1, x_23);
return x_38;
}
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_mkInjectiveTheorems___spec__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_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_mkInjectiveTheorems___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8; uint8_t x_9;
@ -4907,7 +4784,7 @@ return x_15;
}
}
}
static lean_object* _init_l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2___closed__1() {
static lean_object* _init_l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1___closed__1() {
_start:
{
lean_object* x_1;
@ -4915,16 +4792,16 @@ x_1 = lean_mk_string("' is not a constructor");
return x_1;
}
}
static lean_object* _init_l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2___closed__2() {
static lean_object* _init_l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2___closed__1;
x_1 = l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1___closed__1;
x_2 = l_Lean_stringToMessageData(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__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_EXPORT lean_object* l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
@ -4981,11 +4858,11 @@ x_19 = l___private_Lean_Meta_Injective_0__Lean_Meta_mkInjectiveTheoremTypeCore_x
x_20 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_18);
x_21 = l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2___closed__2;
x_21 = l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1___closed__2;
x_22 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
x_23 = l_Lean_throwError___at_Lean_Meta_mkInjectiveTheorems___spec__3(x_22, x_2, x_3, x_4, x_5, x_15);
x_23 = l_Lean_throwError___at_Lean_Meta_mkInjectiveTheorems___spec__2(x_22, x_2, x_3, x_4, x_5, x_15);
return x_23;
}
}
@ -5014,7 +4891,7 @@ return x_27;
}
}
}
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkInjectiveTheorems___spec__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_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkInjectiveTheorems___spec__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) {
_start:
{
if (lean_obj_tag(x_1) == 0)
@ -5038,7 +4915,7 @@ lean_inc(x_9);
x_10 = lean_ctor_get(x_1, 1);
lean_inc(x_10);
lean_dec(x_1);
x_11 = l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2(x_9, x_3, x_4, x_5, x_6, x_7);
x_11 = l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1(x_9, x_3, x_4, x_5, x_6, x_7);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16;
@ -5185,7 +5062,7 @@ return x_36;
LEAN_EXPORT lean_object* l_Lean_Meta_mkInjectiveTheorems(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13;
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_7 = lean_st_ref_get(x_5, x_6);
x_8 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
@ -5197,8 +5074,15 @@ lean_inc(x_10);
lean_dec(x_8);
x_11 = lean_ctor_get(x_4, 0);
lean_inc(x_11);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_1);
x_12 = l_Lean_isInductivePredicate___at_Lean_Meta_mkInjectiveTheorems___spec__1(x_1, x_2, x_3, x_4, x_5, x_9);
x_12 = l_Lean_Meta_isInductivePredicate(x_1, x_2, x_3, x_4, x_5, x_9);
if (lean_obj_tag(x_12) == 0)
{
uint8_t x_13;
x_13 = !lean_is_exclusive(x_12);
if (x_13 == 0)
{
@ -5266,7 +5150,7 @@ x_27 = lean_ctor_get(x_24, 4);
lean_inc(x_27);
lean_dec(x_24);
x_28 = lean_box(0);
x_29 = l_List_forIn_loop___at_Lean_Meta_mkInjectiveTheorems___spec__4(x_27, x_28, x_2, x_3, x_4, x_5, x_26);
x_29 = l_List_forIn_loop___at_Lean_Meta_mkInjectiveTheorems___spec__3(x_27, x_28, x_2, x_3, x_4, x_5, x_26);
if (lean_obj_tag(x_29) == 0)
{
uint8_t x_30;
@ -5460,7 +5344,7 @@ x_64 = lean_ctor_get(x_61, 4);
lean_inc(x_64);
lean_dec(x_61);
x_65 = lean_box(0);
x_66 = l_List_forIn_loop___at_Lean_Meta_mkInjectiveTheorems___spec__4(x_64, x_65, x_2, x_3, x_4, x_5, x_63);
x_66 = l_List_forIn_loop___at_Lean_Meta_mkInjectiveTheorems___spec__3(x_64, x_65, x_2, x_3, x_4, x_5, x_63);
if (lean_obj_tag(x_66) == 0)
{
lean_object* x_67; lean_object* x_68; lean_object* x_69;
@ -5584,12 +5468,42 @@ return x_83;
}
}
}
else
{
uint8_t x_84;
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_84 = !lean_is_exclusive(x_12);
if (x_84 == 0)
{
return x_12;
}
LEAN_EXPORT lean_object* l_Lean_isInductivePredicate___at_Lean_Meta_mkInjectiveTheorems___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
else
{
lean_object* x_85; lean_object* x_86; lean_object* x_87;
x_85 = lean_ctor_get(x_12, 0);
x_86 = lean_ctor_get(x_12, 1);
lean_inc(x_86);
lean_inc(x_85);
lean_dec(x_12);
x_87 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_87, 0, x_85);
lean_ctor_set(x_87, 1, x_86);
return x_87;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_mkInjectiveTheorems___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_Lean_isInductivePredicate___at_Lean_Meta_mkInjectiveTheorems___spec__1(x_1, x_2, x_3, x_4, x_5, x_6);
x_7 = l_Lean_throwError___at_Lean_Meta_mkInjectiveTheorems___spec__2(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
@ -5597,23 +5511,11 @@ lean_dec(x_2);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_mkInjectiveTheorems___spec__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_EXPORT lean_object* l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_Lean_throwError___at_Lean_Meta_mkInjectiveTheorems___spec__3(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2(x_1, x_2, x_3, x_4, x_5, x_6);
x_7 = l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
@ -5741,10 +5643,10 @@ if (lean_io_result_is_error(res)) return res;
l_Lean_Meta_genInjectivity = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Meta_genInjectivity);
lean_dec_ref(res);
l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2___closed__1 = _init_l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2___closed__1();
lean_mark_persistent(l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2___closed__1);
l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2___closed__2 = _init_l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2___closed__2();
lean_mark_persistent(l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__2___closed__2);
l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1___closed__1 = _init_l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1___closed__1();
lean_mark_persistent(l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1___closed__1);
l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1___closed__2 = _init_l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1___closed__2();
lean_mark_persistent(l_Lean_getConstInfoCtor___at_Lean_Meta_mkInjectiveTheorems___spec__1___closed__2);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

255
stage0/stdlib/Lean/Meta/SizeOf.c generated
View file

@ -53,13 +53,13 @@ lean_object* l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_getParamNames___
LEAN_EXPORT lean_object* l_panic___at___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors___spec__1(lean_object*);
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkMinorProof___closed__3;
LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___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_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfFns___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof___spec__2___closed__1;
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLocalDeclImp___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_mkSizeOfFn___lambda__2___closed__2;
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___lambda__3___closed__2;
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorem___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_environment_find(lean_object*, lean_object*);
lean_object* l_Lean_addTrace_addTraceOptions(lean_object*);
@ -129,18 +129,17 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinor
static lean_object* l_List_head_x21___at_Lean_Meta_mkSizeOfFns___spec__3___closed__2;
static lean_object* l_Lean_Meta_mkSizeOfSpecLemmaInstance___closed__4;
LEAN_EXPORT lean_object* l_Lean_Meta_mkSizeOfFn___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_object*, lean_object*, lean_object*);
static lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__2___closed__2;
lean_object* l_Lean_mkAppN(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_mkSizeOfFns___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors_loop___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*);
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkMinorProof___closed__1;
LEAN_EXPORT lean_object* l_Lean_throwKernelException___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isInductivePredicate(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addTrace___at___private_Lean_Meta_LevelDefEq_0__Lean_Meta_postponeIsLevelDefEq___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_addTrace___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkMinorProof___spec__1___closed__5;
LEAN_EXPORT lean_object* l_Lean_getConstInfoInduct___at_Lean_Meta_mkSizeOfFns___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_genSizeOfSpec;
static lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__2___closed__1;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Meta_mkSizeOfSpecLemmaInstance___spec__1(size_t, size_t, lean_object*);
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors___rarg___closed__3;
lean_object* l_Lean_RecursorVal_getMajorIdx(lean_object*);
@ -170,7 +169,6 @@ lean_object* l_Lean_Meta_mkEqSymm(lean_object*, lean_object*, lean_object*, lean
LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof___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 uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Meta_SizeOf_0__Lean_Meta_isInductiveHypothesis_x3f___spec__2(lean_object*, lean_object*, size_t, size_t);
lean_object* l_Lean_KernelException_toMessageData(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___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_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkLocalInstances___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_mkSizeOfSpecLemmaInstance(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorem(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -198,6 +196,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMotiv
static lean_object* l_panic___at___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors___spec__1___rarg___closed__1;
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___spec__6(lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors_loop___rarg___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___private_Lean_Meta_SizeOf_0__Lean_Meta_isRecField_x3f___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -221,15 +220,11 @@ static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_r
uint8_t l_Lean_Expr_isAppOfArity(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkMinorProofStep___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedExpr;
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___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_EXPORT lean_object* l_Lean_Meta_mkSizeOfFn___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*);
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___lambda__2___closed__2;
static lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___boxed(lean_object**);
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkLocalInstances_loop___rarg___lambda__1___closed__1;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof_mkSizeOf___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_isInductivePredicate_visit(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkLocalInstances_loop___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_find___at___private_Lean_Hygiene_0__Lean_sanitizeSyntaxAux___spec__2(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Meta_SizeOf_0__Lean_Meta_isInductiveHypothesis_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -239,11 +234,11 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkLocalInstan
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors_loop___rarg___lambda__2___closed__2;
static lean_object* l_List_head_x21___at_Lean_Meta_mkSizeOfFns___spec__3___closed__3;
LEAN_EXPORT lean_object* l_Lean_Meta_mkSizeOfSpecLemmaInstance___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___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_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors___rarg___closed__6;
LEAN_EXPORT lean_object* l_Lean_Meta_mkSizeOfSpecLemmaName___boxed(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof___lambda__2___boxed__const__1;
static lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__1;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof___spec__5___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*);
uint8_t l_Lean_Expr_isForall(lean_object*);
lean_object* lean_whnf(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -253,14 +248,15 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_SizeO
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkLocalInstances_loop___rarg___lambda__1___closed__2;
static lean_object* l_Lean_Meta_mkSizeOfFn___closed__1;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof___spec__6(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___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_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_recToSizeOf___closed__1;
size_t lean_usize_of_nat(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_SizeOfSpecNested_throwUnexpected___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ConstantInfo_type(lean_object*);
lean_object* l_Lean_setEnv___at_Lean_Meta_setInlineAttribute___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMotives_loop(lean_object*);
static lean_object* l_Lean_Meta_SizeOfSpecNested_throwFailed___rarg___closed__1;
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___boxed(lean_object**);
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkMinorProofStep___closed__2;
LEAN_EXPORT lean_object* l_Lean_Meta_mkSizeOfFn___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_genSizeOf___closed__1;
@ -282,8 +278,6 @@ static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_m
lean_object* lean_name_append_after(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkMinorProof___lambda__1___closed__6;
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___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_Lean_isInductivePredicate___at_Lean_Meta_mkSizeOfInstances___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwKernelException___at_Lean_Meta_mkSizeOfFn___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMotives_loop___rarg___lambda__1___closed__3;
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors___rarg___closed__5;
@ -344,6 +338,7 @@ static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMotives_lo
static lean_object* l_Lean_Meta_SizeOfSpecNested_throwUnexpected___rarg___closed__4;
LEAN_EXPORT lean_object* l_Lean_getConstInfo___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*);
static lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2___closed__2;
LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_infer_type(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*);
@ -375,8 +370,8 @@ LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6348_(
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_5807_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_5784_(lean_object*);
LEAN_EXPORT lean_object* l_Subarray_forInUnsafe_loop___at___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorem___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_isInductivePredicate___at_Lean_Meta_mkSizeOfInstances___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_SizeOfSpecNested_throwFailed___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2___closed__1;
LEAN_EXPORT lean_object* l_Lean_getConstInfoRec___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemmaProof___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors_loop___rarg___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_Meta_mkSizeOfFn___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -394,8 +389,8 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNes
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMotives_loop___rarg___lambda__1___closed__2;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorems___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_levelOne;
static lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__3;
lean_object* l_Lean_Meta_mkEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__3;
lean_object* l_Lean_indentExpr(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMotives_loop___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfMinors___rarg___closed__4;
@ -413,13 +408,16 @@ static lean_object* l_Lean_addTrace___at___private_Lean_Meta_SizeOf_0__Lean_Meta
LEAN_EXPORT lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_mkSizeOfSpecLemmaName___closed__1;
LEAN_EXPORT lean_object* l_Lean_addDecl___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___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*);
static lean_object* l_Lean_getConstInfoRec___at_Lean_Meta_mkSizeOfFn___spec__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescopeReducing___at___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___spec__7___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_getConstInfoRec___at_Lean_Meta_mkSizeOfFn___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at_Lean_Meta_mkSizeOfFns___spec__5___boxed(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_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__2;
lean_object* l_Lean_Meta_instInhabitedMetaM___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkAdd(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_mkSizeOfSpecLemmaInstance___closed__2;
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkNumeral(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_SizeOf_0__Lean_Meta_SizeOfSpecNested_mkSizeOfAuxLemma___lambda__2___closed__1;
LEAN_EXPORT lean_object* l_Lean_getConstInfoCtor___at___private_Lean_Meta_SizeOf_0__Lean_Meta_mkSizeOfSpecTheorem___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -14304,127 +14302,7 @@ x_4 = l_Lean_Option_register___at_Std_Format_initFn____x40_Lean_Data_Format___hy
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_isInductivePredicate___at_Lean_Meta_mkSizeOfInstances___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; uint8_t x_8;
x_7 = lean_st_ref_get(x_5, x_6);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = lean_ctor_get(x_7, 0);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
lean_dec(x_9);
x_11 = lean_environment_find(x_10, x_1);
if (lean_obj_tag(x_11) == 0)
{
uint8_t x_12; lean_object* x_13;
x_12 = 0;
x_13 = lean_box(x_12);
lean_ctor_set(x_7, 0, x_13);
return x_7;
}
else
{
lean_object* x_14;
x_14 = lean_ctor_get(x_11, 0);
lean_inc(x_14);
lean_dec(x_11);
if (lean_obj_tag(x_14) == 5)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19;
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
lean_dec(x_14);
x_16 = lean_ctor_get(x_15, 0);
lean_inc(x_16);
lean_dec(x_15);
x_17 = lean_ctor_get(x_16, 2);
lean_inc(x_17);
lean_dec(x_16);
x_18 = l_Lean_isInductivePredicate_visit(x_17);
lean_dec(x_17);
x_19 = lean_box(x_18);
lean_ctor_set(x_7, 0, x_19);
return x_7;
}
else
{
uint8_t x_20; lean_object* x_21;
lean_dec(x_14);
x_20 = 0;
x_21 = lean_box(x_20);
lean_ctor_set(x_7, 0, x_21);
return x_7;
}
}
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_22 = lean_ctor_get(x_7, 0);
x_23 = lean_ctor_get(x_7, 1);
lean_inc(x_23);
lean_inc(x_22);
lean_dec(x_7);
x_24 = lean_ctor_get(x_22, 0);
lean_inc(x_24);
lean_dec(x_22);
x_25 = lean_environment_find(x_24, x_1);
if (lean_obj_tag(x_25) == 0)
{
uint8_t x_26; lean_object* x_27; lean_object* x_28;
x_26 = 0;
x_27 = lean_box(x_26);
x_28 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_28, 0, x_27);
lean_ctor_set(x_28, 1, x_23);
return x_28;
}
else
{
lean_object* x_29;
x_29 = lean_ctor_get(x_25, 0);
lean_inc(x_29);
lean_dec(x_25);
if (lean_obj_tag(x_29) == 5)
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; uint8_t x_33; lean_object* x_34; lean_object* x_35;
x_30 = lean_ctor_get(x_29, 0);
lean_inc(x_30);
lean_dec(x_29);
x_31 = lean_ctor_get(x_30, 0);
lean_inc(x_31);
lean_dec(x_30);
x_32 = lean_ctor_get(x_31, 2);
lean_inc(x_32);
lean_dec(x_31);
x_33 = l_Lean_isInductivePredicate_visit(x_32);
lean_dec(x_32);
x_34 = lean_box(x_33);
x_35 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_35, 0, x_34);
lean_ctor_set(x_35, 1, x_23);
return x_35;
}
else
{
uint8_t x_36; lean_object* x_37; lean_object* x_38;
lean_dec(x_29);
x_36 = 0;
x_37 = lean_box(x_36);
x_38 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_38, 0, x_37);
lean_ctor_set(x_38, 1, x_23);
return x_38;
}
}
}
}
}
static lean_object* _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__1() {
static lean_object* _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__1() {
_start:
{
lean_object* x_1;
@ -14432,7 +14310,7 @@ x_1 = lean_mk_string("mk");
return x_1;
}
}
static lean_object* _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__2() {
static lean_object* _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__2() {
_start:
{
lean_object* x_1;
@ -14440,17 +14318,17 @@ x_1 = lean_mk_string("_sizeOf_inst");
return x_1;
}
}
static lean_object* _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__3() {
static lean_object* _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__2;
x_2 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__2;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14, lean_object* x_15, lean_object* x_16, lean_object* x_17) {
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14, lean_object* x_15, lean_object* x_16, lean_object* x_17) {
_start:
{
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; uint8_t x_25; uint8_t x_26; lean_object* x_27;
@ -14476,7 +14354,7 @@ lean_inc(x_28);
x_29 = lean_ctor_get(x_27, 1);
lean_inc(x_29);
lean_dec(x_27);
x_30 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__1;
x_30 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__1;
x_31 = lean_name_mk_string(x_7, x_30);
x_32 = lean_array_push(x_1, x_28);
lean_inc(x_16);
@ -14492,7 +14370,7 @@ lean_inc(x_34);
x_35 = lean_ctor_get(x_33, 1);
lean_inc(x_35);
lean_dec(x_33);
x_36 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__3;
x_36 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__3;
x_37 = l_Lean_Name_append(x_8, x_36);
x_38 = l_Array_append___rarg(x_9, x_5);
lean_inc(x_13);
@ -14697,7 +14575,7 @@ return x_74;
}
}
}
static lean_object* _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__2___closed__1() {
static lean_object* _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2___closed__1() {
_start:
{
lean_object* x_1;
@ -14705,17 +14583,17 @@ x_1 = lean_mk_string("m");
return x_1;
}
}
static lean_object* _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__2___closed__2() {
static lean_object* _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__2___closed__1;
x_2 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___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_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
_start:
{
lean_object* x_14; 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;
@ -14747,7 +14625,7 @@ lean_inc(x_22);
x_23 = lean_ctor_get(x_21, 1);
lean_inc(x_23);
lean_dec(x_21);
x_24 = lean_alloc_closure((void*)(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___boxed), 17, 11);
x_24 = lean_alloc_closure((void*)(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___boxed), 17, 11);
lean_closure_set(x_24, 0, x_19);
lean_closure_set(x_24, 1, x_5);
lean_closure_set(x_24, 2, x_16);
@ -14759,7 +14637,7 @@ lean_closure_set(x_24, 7, x_2);
lean_closure_set(x_24, 8, x_3);
lean_closure_set(x_24, 9, x_22);
lean_closure_set(x_24, 10, x_14);
x_25 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__2___closed__2;
x_25 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2___closed__2;
x_26 = 0;
x_27 = l_Lean_Meta_withLocalDecl___at___private_Lean_Meta_SizeOf_0__Lean_Meta_mkLocalInstances_loop___spec__1___rarg(x_25, x_26, x_18, x_24, x_9, x_10, x_11, x_12, x_23);
return x_27;
@ -14802,7 +14680,7 @@ return x_31;
}
}
}
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___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_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___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) {
_start:
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
@ -14818,7 +14696,7 @@ lean_inc(x_6);
x_17 = l_Array_toSubarray___rarg(x_6, x_13, x_16);
x_18 = l_Array_ofSubarray___rarg(x_15);
lean_inc(x_18);
x_19 = lean_alloc_closure((void*)(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__2), 13, 7);
x_19 = lean_alloc_closure((void*)(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2), 13, 7);
lean_closure_set(x_19, 0, x_2);
lean_closure_set(x_19, 1, x_3);
lean_closure_set(x_19, 2, x_6);
@ -14830,7 +14708,7 @@ x_20 = l___private_Lean_Meta_SizeOf_0__Lean_Meta_mkLocalInstances___rarg(x_18, x
return x_20;
}
}
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__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_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
if (lean_obj_tag(x_2) == 0)
@ -14912,7 +14790,7 @@ lean_dec(x_24);
x_28 = lean_ctor_get(x_26, 2);
lean_inc(x_28);
lean_inc(x_1);
x_29 = lean_alloc_closure((void*)(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__3___boxed), 12, 5);
x_29 = lean_alloc_closure((void*)(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__3___boxed), 12, 5);
lean_closure_set(x_29, 0, x_25);
lean_closure_set(x_29, 1, x_26);
lean_closure_set(x_29, 2, x_10);
@ -15022,7 +14900,7 @@ lean_dec(x_45);
x_49 = lean_ctor_get(x_47, 2);
lean_inc(x_49);
lean_inc(x_1);
x_50 = lean_alloc_closure((void*)(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__3___boxed), 12, 5);
x_50 = lean_alloc_closure((void*)(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__3___boxed), 12, 5);
lean_closure_set(x_50, 0, x_46);
lean_closure_set(x_50, 1, x_47);
lean_closure_set(x_50, 2, x_10);
@ -15117,7 +14995,7 @@ return x_61;
LEAN_EXPORT lean_object* l_Lean_Meta_mkSizeOfInstances(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13;
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_7 = lean_st_ref_get(x_5, x_6);
x_8 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
@ -15129,8 +15007,15 @@ lean_inc(x_10);
lean_dec(x_8);
x_11 = lean_ctor_get(x_4, 0);
lean_inc(x_11);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_1);
x_12 = l_Lean_isInductivePredicate___at_Lean_Meta_mkSizeOfInstances___spec__1(x_1, x_2, x_3, x_4, x_5, x_9);
x_12 = l_Lean_Meta_isInductivePredicate(x_1, x_2, x_3, x_4, x_5, x_9);
if (lean_obj_tag(x_12) == 0)
{
uint8_t x_13;
x_13 = !lean_is_exclusive(x_12);
if (x_13 == 0)
{
@ -15225,7 +15110,7 @@ lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_35);
x_36 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2(x_16, x_35, x_34, x_2, x_3, x_4, x_5, x_29);
x_36 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1(x_16, x_35, x_34, x_2, x_3, x_4, x_5, x_29);
if (lean_obj_tag(x_36) == 0)
{
uint8_t x_37;
@ -15542,7 +15427,7 @@ lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_98);
x_99 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2(x_77, x_98, x_97, x_2, x_3, x_4, x_5, x_92);
x_99 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1(x_77, x_98, x_97, x_2, x_3, x_4, x_5, x_92);
if (lean_obj_tag(x_99) == 0)
{
lean_object* x_100; lean_object* x_101; lean_object* x_102; uint8_t x_103;
@ -15737,20 +15622,38 @@ return x_127;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_isInductivePredicate___at_Lean_Meta_mkSizeOfInstances___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
else
{
lean_object* x_7;
x_7 = l_Lean_isInductivePredicate___at_Lean_Meta_mkSizeOfInstances___spec__1(x_1, x_2, x_3, x_4, x_5, x_6);
uint8_t x_128;
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_7;
lean_dec(x_1);
x_128 = !lean_is_exclusive(x_12);
if (x_128 == 0)
{
return x_12;
}
else
{
lean_object* x_129; lean_object* x_130; lean_object* x_131;
x_129 = lean_ctor_get(x_12, 0);
x_130 = lean_ctor_get(x_12, 1);
lean_inc(x_130);
lean_inc(x_129);
lean_dec(x_12);
x_131 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_131, 0, x_129);
lean_ctor_set(x_131, 1, x_130);
return x_131;
}
}
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___boxed(lean_object** _args) {
}
}
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___boxed(lean_object** _args) {
lean_object* x_1 = _args[0];
lean_object* x_2 = _args[1];
lean_object* x_3 = _args[2];
@ -15771,16 +15674,16 @@ lean_object* x_17 = _args[16];
_start:
{
lean_object* x_18;
x_18 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1(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, x_16, x_17);
x_18 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1(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, x_16, x_17);
lean_dec(x_8);
return x_18;
}
}
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___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_EXPORT lean_object* l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___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) {
_start:
{
lean_object* x_13;
x_13 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___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 = l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___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);
lean_dec(x_7);
return x_13;
}
@ -16039,16 +15942,16 @@ if (lean_io_result_is_error(res)) return res;
l_Lean_Meta_genSizeOfSpec = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Meta_genSizeOfSpec);
lean_dec_ref(res);
l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__1 = _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__1();
lean_mark_persistent(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__1);
l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__2 = _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__2();
lean_mark_persistent(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__2);
l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__3 = _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__3();
lean_mark_persistent(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__1___closed__3);
l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__2___closed__1 = _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__2___closed__1();
lean_mark_persistent(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__2___closed__1);
l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__2___closed__2 = _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__2___closed__2();
lean_mark_persistent(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__2___lambda__2___closed__2);
l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__1 = _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__1();
lean_mark_persistent(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__1);
l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__2 = _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__2();
lean_mark_persistent(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__2);
l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__3 = _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__3();
lean_mark_persistent(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__1___closed__3);
l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2___closed__1 = _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2___closed__1();
lean_mark_persistent(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2___closed__1);
l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2___closed__2 = _init_l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2___closed__2();
lean_mark_persistent(l_List_forIn_loop___at_Lean_Meta_mkSizeOfInstances___spec__1___lambda__2___closed__2);
res = l_Lean_Meta_initFn____x40_Lean_Meta_SizeOf___hyg_6348_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

136
stage0/stdlib/Lean/MonadEnv.c generated
View file

@ -74,7 +74,6 @@ LEAN_EXPORT lean_object* l_List_foldlM___at___private_Lean_MonadEnv_0__Lean_chec
LEAN_EXPORT lean_object* l_Lean_addAndCompile___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_MonadEnv_0__Lean_supportedRecursors___closed__10;
static lean_object* l___private_Lean_MonadEnv_0__Lean_supportedRecursors___closed__32;
extern lean_object* l_Lean_levelZero;
lean_object* lean_nat_add(lean_object*, lean_object*);
static lean_object* l_Lean_getConstInfo___rarg___lambda__1___closed__3;
LEAN_EXPORT lean_object* l_Lean_getConstInfoCtor___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
@ -126,7 +125,6 @@ static lean_object* l___private_Lean_MonadEnv_0__Lean_supportedRecursors___close
LEAN_EXPORT lean_object* l_Lean_matchConstInduct(lean_object*, lean_object*);
static lean_object* l___private_Lean_MonadEnv_0__Lean_supportedRecursors___closed__26;
LEAN_EXPORT lean_object* l_List_foldlM___at___private_Lean_MonadEnv_0__Lean_checkUnsupported___spec__3___rarg___lambda__1(lean_object*, lean_object*, lean_object*, size_t, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_isInductivePredicate_visit(lean_object*);
LEAN_EXPORT lean_object* l_Lean_findModuleOf_x3f___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_getConstInfo(lean_object*);
static lean_object* l___private_Lean_MonadEnv_0__Lean_supportedRecursors___closed__19;
@ -152,7 +150,6 @@ LEAN_EXPORT lean_object* l_Lean_addDecl___rarg___lambda__1___boxed(lean_object*,
static lean_object* l___private_Lean_MonadEnv_0__Lean_supportedRecursors___closed__12;
LEAN_EXPORT lean_object* l_Lean_withoutModifyingEnv___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_mkAuxName___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_isInductivePredicate___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Declaration_foldExprM___at___private_Lean_MonadEnv_0__Lean_checkUnsupported___spec__1___rarg___boxed__const__1;
LEAN_EXPORT lean_object* l_Lean_mkAuxName___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_evalConstCheck___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -178,7 +175,6 @@ lean_object* l_Lean_Environment_getModuleIdxFor_x3f(lean_object*, lean_object*);
static lean_object* l_Lean_getConstInfoCtor___rarg___lambda__1___closed__2;
static lean_object* l___private_Lean_MonadEnv_0__Lean_supportedRecursors___closed__33;
static lean_object* l___private_Lean_MonadEnv_0__Lean_supportedRecursors___closed__13;
LEAN_EXPORT lean_object* l_Lean_isInductivePredicate_visit___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Declaration_foldExprM___at___private_Lean_MonadEnv_0__Lean_checkUnsupported___spec__1___rarg___lambda__1(lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_matchConstInduct___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_compileDecl___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -191,7 +187,6 @@ LEAN_EXPORT lean_object* l___private_Lean_MonadEnv_0__Lean_mkAuxNameAux(lean_obj
static lean_object* l_Lean_getConstInfoRec___rarg___lambda__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_ofExcept___at_Lean_evalConstCheck___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_List_allM___at_Lean_isEnumType___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Lean_isInductivePredicate___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_matchConstStruct(lean_object*, lean_object*);
static lean_object* l_Lean_getConstInfoRec___rarg___lambda__1___closed__2;
LEAN_EXPORT lean_object* l_Lean_findModuleOf_x3f___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -208,14 +203,12 @@ uint8_t l_List_isEmpty___rarg(lean_object*);
lean_object* l_Lean_mkLevelParam(lean_object*);
LEAN_EXPORT lean_object* l_List_allM___at_Lean_isEnumType___spec__1___rarg___lambda__1(lean_object*, lean_object*);
static lean_object* l___private_Lean_MonadEnv_0__Lean_supportedRecursors___closed__17;
uint8_t lean_level_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_MonadEnv_0__Lean_checkUnsupported___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_MonadEnv_0__Lean_supportedRecursors___closed__27;
LEAN_EXPORT lean_object* l_Lean_getConstInfoCtor(lean_object*);
LEAN_EXPORT lean_object* l_List_foldlM___at___private_Lean_MonadEnv_0__Lean_checkUnsupported___spec__2___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_matchConstCtor(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_isInductivePredicate(lean_object*);
static lean_object* l___private_Lean_MonadEnv_0__Lean_supportedRecursors___closed__9;
LEAN_EXPORT lean_object* l___private_Lean_MonadEnv_0__Lean_supportedRecursors;
LEAN_EXPORT lean_object* l_Lean_matchConstCtor___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -348,135 +341,6 @@ x_2 = lean_alloc_closure((void*)(l_Lean_isInductive___rarg), 3, 0);
return x_2;
}
}
LEAN_EXPORT uint8_t l_Lean_isInductivePredicate_visit(lean_object* x_1) {
_start:
{
switch (lean_obj_tag(x_1)) {
case 3:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4;
x_2 = lean_ctor_get(x_1, 0);
x_3 = l_Lean_levelZero;
x_4 = lean_level_eq(x_2, x_3);
return x_4;
}
case 7:
{
lean_object* x_5;
x_5 = lean_ctor_get(x_1, 2);
x_1 = x_5;
goto _start;
}
default:
{
uint8_t x_7;
x_7 = 0;
return x_7;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_isInductivePredicate_visit___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_isInductivePredicate_visit(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_isInductivePredicate___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_environment_find(x_3, x_1);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_5; lean_object* x_6; uint8_t x_7; lean_object* x_8; lean_object* x_9;
x_5 = lean_ctor_get(x_2, 0);
lean_inc(x_5);
lean_dec(x_2);
x_6 = lean_ctor_get(x_5, 1);
lean_inc(x_6);
lean_dec(x_5);
x_7 = 0;
x_8 = lean_box(x_7);
x_9 = lean_apply_2(x_6, lean_box(0), x_8);
return x_9;
}
else
{
lean_object* x_10;
x_10 = lean_ctor_get(x_4, 0);
lean_inc(x_10);
lean_dec(x_4);
if (lean_obj_tag(x_10) == 5)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
lean_dec(x_10);
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
lean_dec(x_11);
x_13 = lean_ctor_get(x_12, 2);
lean_inc(x_13);
lean_dec(x_12);
x_14 = lean_ctor_get(x_2, 0);
lean_inc(x_14);
lean_dec(x_2);
x_15 = lean_ctor_get(x_14, 1);
lean_inc(x_15);
lean_dec(x_14);
x_16 = l_Lean_isInductivePredicate_visit(x_13);
lean_dec(x_13);
x_17 = lean_box(x_16);
x_18 = lean_apply_2(x_15, lean_box(0), x_17);
return x_18;
}
else
{
lean_object* x_19; lean_object* x_20; uint8_t x_21; lean_object* x_22; lean_object* x_23;
lean_dec(x_10);
x_19 = lean_ctor_get(x_2, 0);
lean_inc(x_19);
lean_dec(x_2);
x_20 = lean_ctor_get(x_19, 1);
lean_inc(x_20);
lean_dec(x_19);
x_21 = 0;
x_22 = lean_box(x_21);
x_23 = lean_apply_2(x_20, lean_box(0), x_22);
return x_23;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_isInductivePredicate___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
x_5 = lean_ctor_get(x_2, 0);
lean_inc(x_5);
lean_dec(x_2);
x_6 = lean_alloc_closure((void*)(l_Lean_isInductivePredicate___rarg___lambda__1), 3, 2);
lean_closure_set(x_6, 0, x_3);
lean_closure_set(x_6, 1, x_1);
x_7 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_5, x_6);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Lean_isInductivePredicate(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_isInductivePredicate___rarg), 3, 0);
return x_2;
}
}
LEAN_EXPORT uint8_t l_Lean_isRecCore(lean_object* x_1, lean_object* x_2) {
_start:
{