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:
Sebastian Ullrich 2022-07-20 20:59:57 +02:00
parent 15bb3ccf6b
commit b5417bdc6c
190 changed files with 77316 additions and 48252 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1067,6 +1067,12 @@ def TSepArray.push (sa : TSepArray k sep) (e : TSyntax k) : TSepArray k sep :=
else
{ elemsAndSeps := sa.elemsAndSeps.push (mkAtom sep) |>.push e }
instance : EmptyCollection (SepArray sep) where
emptyCollection := ⟨∅⟩
instance : EmptyCollection (TSepArray sep k) where
emptyCollection := ⟨∅⟩
/-
We use `CoeTail` here instead of `Coe` to avoid a "loop" when computing `CoeTC`.
The "loop" is interrupted using the maximum instance size threshold, but it is a performance bottleneck.

9
stage0/src/Init/Util.lean generated
View file

@ -42,8 +42,15 @@ unsafe def ptrAddrUnsafe {α : Type u} (a : @& α) : USize := 0
@[inline] unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=
k (ptrAddrUnsafe a)
@[inline] unsafe def ptrEq (a b : α) : Bool := ptrAddrUnsafe a == ptrAddrUnsafe b
unsafe def ptrEqList : (as bs : List α) → Bool
| [], [] => true
| a::as, b::bs => if ptrEq a b then ptrEqList as bs else false
| _, _ => false
@[inline] unsafe def withPtrEqUnsafe {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=
if ptrAddrUnsafe a == ptrAddrUnsafe b then true else k ()
if ptrEq a b then true else k ()
@[implementedBy withPtrEqUnsafe]
def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool := k ()

11
stage0/src/Lean/Attributes.lean generated
View file

@ -24,6 +24,17 @@ structure AttributeImplCore where
applicationTime := AttributeApplicationTime.afterTypeChecking
deriving Inhabited
/-- You can tag attributes with the 'local' or 'scoped' kind.
For example: `attribute [local myattr, scoped yourattr, theirattr]`.
This is used to indicate how an attribute should be scoped.
- local means that the attribute should only be applied in the current scope and forgotten once the current section, namespace, or file is closed.
- scoped means that the attribute should only be applied while the namespace is open.
- global means that the attribute should always be applied.
Note that the attribute handler (`AttributeImpl.add`) is responsible for interpreting the kind and
making sure that these kinds are respected.
-/
inductive AttributeKind
| «global» | «local» | «scoped»
deriving BEq, Inhabited

37
stage0/src/Lean/Data/Lsp/LanguageFeatures.lean generated
View file

@ -226,11 +226,13 @@ structure SymbolInformation where
deriving ToJson
inductive SemanticTokenType where
-- Used by Lean
| keyword
| «variable»
| property
| function
/-
/- Other types included by default in the LSP specification.
Not used by the Lean core, but useful to users extending the Lean server. -/
| «namespace»
| type
| «class»
@ -249,19 +251,23 @@ inductive SemanticTokenType where
| number
| regexp
| operator
-/
| decorator
-- must be in the same order as the constructors
def SemanticTokenType.names : Array String :=
#["keyword", "variable", "property", "function"]
#["keyword", "variable", "property", "function", "namespace", "type", "class",
"enum", "interface", "struct", "typeParameter", "parameter", "enumMember",
"event", "method", "macro", "modifier", "comment", "string", "number",
"regexp", "operator", "decorator"]
-- must be the correct index in `names`
def SemanticTokenType.toNat : SemanticTokenType → Nat
| keyword => 0
| «variable» => 1
| property => 2
| function => 3
def SemanticTokenType.toNat (type : SemanticTokenType) : Nat :=
type.toCtorIdx
/-
/--
The semantic token modifiers included by default in the LSP specification.
Not used by the Lean core, but implementing them here allows them to be
utilized by users extending the Lean server.
-/
inductive SemanticTokenModifier where
| declaration
| definition
@ -273,7 +279,14 @@ inductive SemanticTokenModifier where
| modification
| documentation
| defaultLibrary
-/
-- must be in the same order as the constructors
def SemanticTokenModifier.names : Array String :=
#["declaration", "definition", "readonly", "static", "deprecated", "abstract",
"async", "modification", "documentation", "defaultLibrary"]
def SemanticTokenModifier.toNat (modifier : SemanticTokenType) : Nat :=
modifier.toCtorIdx
structure SemanticTokensLegend where
tokenTypes : Array String
@ -298,7 +311,7 @@ structure SemanticTokensRangeParams where
deriving FromJson, ToJson
structure SemanticTokens where
-- resultId?: string;
resultId? : Option String := none
data : Array Nat
deriving FromJson, ToJson

2
stage0/src/Lean/Declaration.lean generated
View file

@ -121,7 +121,7 @@ structure TheoremVal extends ConstantVal where
all : List Name := [name]
deriving Inhabited
/- Value for an opaque constant declaration `constant x : t := e` -/
/- Value for an opaque constant declaration `opaque x : t := e` -/
structure OpaqueVal extends ConstantVal where
value : Expr
isUnsafe : Bool

47
stage0/src/Lean/Elab/Declaration.lean generated
View file

@ -13,7 +13,6 @@ import Lean.Elab.DeclarationRange
namespace Lean.Elab.Command
open Meta
open TSyntax.Compat
private def ensureValidNamespace (name : Name) : MacroM Unit := do
match name with
@ -143,7 +142,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
classes ← getOptDerivingClasses decl[5]
else
computedFields ← (decl[5].getOptional?.map (·[1].getArgs) |>.getD #[]).mapM fun cf => withRef cf do
return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := cf[3], matchAlts := cf[4] }
return { ref := cf, modifiers := cf[0], fieldId := cf[1].getId, type := ⟨cf[3]⟩, matchAlts := ⟨cf[4]⟩ }
classes ← getOptDerivingClasses decl[6]
return {
ref := decl
@ -180,7 +179,7 @@ def elabDeclaration : CommandElab := fun stx => do
match (← liftMacroM <| expandDeclNamespace? stx) with
| some (ns, newStx) => do
let ns := mkIdentFrom stx ns
let newStx ← `(namespace $ns:ident $newStx end $ns:ident)
let newStx ← `(namespace $ns:ident $(⟨newStx⟩) end $ns:ident)
withMacroExpansion stx newStx <| elabCommand newStx
| none => do
let decl := stx[1]
@ -260,7 +259,7 @@ def expandMutualNamespace : Macro := fun stx => do
| some ns =>
let ns := mkIdentFrom stx ns
let stxNew := stx.setArg 1 (mkNullNode elemsNew)
`(namespace $ns:ident $stxNew end $ns:ident)
`(namespace $ns:ident $(⟨stxNew⟩) end $ns:ident)
| none => Macro.throwUnsupported
@[builtinMacro Lean.Parser.Command.mutual]
@ -327,35 +326,21 @@ def elabMutual : CommandElab := fun stx => do
for attrName in toErase do
Attribute.erase declName attrName
def expandInitCmd (builtin : Bool) : Macro := fun stx => do
let optVisibility := stx[0]
let optHeader := stx[2]
let doSeq := stx[3]
let attrId := mkIdentFrom stx <| if builtin then `builtinInit else `init
if optHeader.isNone then
unless optVisibility.isNone do
Macro.throwError "invalid initialization command, 'visibility' modifer is not allowed"
`(@[$attrId:ident]def initFn : IO Unit := do $doSeq)
else
let id := optHeader[0]
let type := optHeader[1][1]
if optVisibility.isNone then
@[builtinMacro Lean.Parser.Command.«initialize»] def expandInitialize : Macro
| stx@`($declModifiers:declModifiers $kw:initializeKeyword $[$id? : $type? ←]? $doSeq) => do
let attrId := mkIdentFrom stx <| if kw.raw[0].isToken "initialize" then `init else `builtinInit
if let (some id, some type) := (id?, type?) then
let `(Parser.Command.declModifiersT| $[$doc?:docComment]? $[@[$attrs?,*]]? $(vis?)? $[unsafe%$unsafe?]?) := stx[0]
| Macro.throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
let declModifiers ← `(Parser.Command.declModifiersT| $[$doc?:docComment]? @[$attrId:ident initFn, $(attrs?.getD ∅),*] $(vis?)? $[unsafe%$unsafe?]?)
`(def initFn : IO $type := do $doSeq
@[$attrId:ident initFn] opaque $id : $type)
else if optVisibility[0].getKind == ``Parser.Command.private then
`(def initFn : IO $type := do $doSeq
@[$attrId:ident initFn] private opaque $id : $type)
else if optVisibility[0].getKind == ``Parser.Command.protected then
`(def initFn : IO $type := do $doSeq
@[$attrId:ident initFn] protected opaque $id : $type)
$(⟨declModifiers⟩):declModifiers opaque $id : $type)
else
Macro.throwError "unexpected visibility annotation"
@[builtinMacro Lean.Parser.Command.«initialize»] def expandInitialize : Macro :=
expandInitCmd (builtin := false)
@[builtinMacro Lean.Parser.Command.«builtin_initialize»] def expandBuiltinInitialize : Macro :=
expandInitCmd (builtin := true)
if let `(Parser.Command.declModifiersT| ) := declModifiers then
`(@[$attrId:ident] def initFn : IO Unit := do $doSeq)
else
Macro.throwErrorAt declModifiers "invalid initialization command, unexpected modifiers"
| _ => Macro.throwUnsupported
builtin_initialize
registerTraceClass `Elab.axiom

6
stage0/src/Lean/Elab/Deriving/FromToJson.lean generated
View file

@ -30,7 +30,7 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
let (isOptField, nm) := mkJsonField field
if isOptField then ``(opt $nm $(mkIdent <| header.targetNames[0]! ++ field))
else ``([($nm, toJson $(mkIdent <| header.targetNames[0]! ++ field))])
let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]!):ident $header.binders:bracketedBinder* :=
let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]!):ident $header.binders:bracketedBinder* : Json :=
mkObj <| List.join [$fields,*])
return #[cmd] ++ (← mkInstanceCmds ctx ``ToJson declNames)
cmds.forM elabCommand
@ -63,9 +63,9 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
if ctx.usePartial then
let letDecls ← mkLocalInstanceLetDecls ctx ``ToJson header.argNames
let auxTerm ← mkLet letDecls auxTerm
`(private partial def $toJsonFuncId:ident $header.binders:bracketedBinder* := $auxTerm)
`(private partial def $toJsonFuncId:ident $header.binders:bracketedBinder* : Json := $auxTerm)
else
`(private def $toJsonFuncId:ident $header.binders:bracketedBinder* := $auxTerm)
`(private def $toJsonFuncId:ident $header.binders:bracketedBinder* : Json := $auxTerm)
return #[auxCmd] ++ (← mkInstanceCmds ctx ``ToJson declNames)
cmds.forM elabCommand
return true

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

@ -500,7 +500,7 @@ private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr
Term.synthesizeSyntheticMVarsNoPostponing
-- TODO: add forbidden predicate using `shortDeclName` from `view`
let params ← Term.addAutoBoundImplicits params
let value ← Term.elabTerm valStx none
let value ← Term.withoutAutoBoundImplicit <| Term.elabTerm valStx none
let value ← mkLambdaFVars params value
return (none, value)
| some typeStx =>
@ -512,7 +512,7 @@ private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr
let type ← mkForallFVars params type
return (type, none)
| some valStx =>
let value ← Term.elabTermEnsuringType valStx type
let value ← Term.withoutAutoBoundImplicit <| Term.elabTermEnsuringType valStx type
Term.synthesizeSyntheticMVarsNoPostponing
let type ← mkForallFVars params type
let value ← mkLambdaFVars params value

113
stage0/src/Lean/Elab/Tactic/Basic.lean generated
View file

@ -131,68 +131,85 @@ def mkInitialTacticInfo (stx : Syntax) : TacticM (TacticM Info) := do
withInfoContext x (← mkInitialTacticInfo stx)
/-
Important: we must define `evalTacticUsing` and `expandTacticMacroFns` before we define
Important: we must define `evalTactic` before we define
the instance `MonadExcept` for `TacticM` since it backtracks the state including error messages,
and this is bad when rethrowing the exception at the `catch` block in these methods.
We marked these places with a `(*)` in these methods.
-/
private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List (KeyedDeclsAttribute.AttributeEntry Tactic)) : TacticM Unit := do
let rec loop
| [] => throwErrorAt stx "unexpected syntax {indentD stx}"
| evalFn::evalFns => do
try
withReader ({ · with elaborator := evalFn.declName }) <| withTacticInfoContext stx <| evalFn.value stx
catch
| ex@(.error ..) =>
match evalFns with
| [] => throw ex -- (*)
| evalFns => s.restore; loop evalFns
| ex@(.internal id _) =>
/--
Auxiliary datastructure for capturing exceptions at `evalTactic`.
-/
inductive EvalTacticFailure where
| /-- Exceptions ≠ AbortException -/
exception (ex : Exception)
| /--
`abort` exceptions are used when exceptions have already been logged at the message Log.
Thus, we save the whole state here to make sure we don't lose them.
-/
abort (s : SavedState)
partial def evalTactic (stx : Syntax) : TacticM Unit :=
withRef stx <| withIncRecDepth <| withFreshMacroScope <| match stx with
| .node _ k _ =>
if k == nullKind then
-- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]`
stx.getArgs.forM evalTactic
else do
trace[Elab.step] "{stx}"
let evalFns := tacticElabAttribute.getEntries (← getEnv) stx.getKind
let macros := macroAttribute.getEntries (← getEnv) stx.getKind
if evalFns.isEmpty && macros.isEmpty then
throwErrorAt stx "tactic '{stx.getKind}' has not been implemented"
let s ← Tactic.saveState
expandEval s macros evalFns #[]
| .missing => pure ()
| _ => throwError m!"unexpected tactic{indentD stx}"
where
throwExs (failures : Array EvalTacticFailure) : TacticM Unit := do
let exs := failures.filterMap fun | .abort _ => none | .exception ex => some ex
if exs.isEmpty then
if let some (.abort s) := failures.find? fun | .abort _ => true | _ => false then
s.restore
throwAbortTactic
else
throwErrorAt stx "unexpected syntax {indentD stx}"
else if h : 0 < exs.size then
throw exs[0] -- (*)
else
withRef stx do throwErrorWithNestedErrors "tactic failed" exs -- (*)
@[inline] handleEx (s : SavedState) (failures : Array EvalTacticFailure) (ex : Exception) (k : Array EvalTacticFailure → TacticM Unit) := do
match ex with
| .error .. => s.restore; k (failures.push (.exception ex))
| .internal id _ =>
if id == unsupportedSyntaxExceptionId then
s.restore; loop evalFns
-- We do not store `unsupportedSyntaxExceptionId`, see throwExs
s.restore; k failures
else if id == abortTacticExceptionId then
let failures := failures.push (.abort (← Tactic.saveState))
s.restore; k failures
else
throw ex
loop tactics
throw ex -- (*)
mutual
partial def expandTacticMacroFns (s : SavedState) (stx : Syntax) (macros : List (KeyedDeclsAttribute.AttributeEntry Macro)) : TacticM Unit :=
let rec loop
| [] => throwErrorAt stx "tactic '{stx.getKind}' has not been implemented"
| m::ms => do
expandEval (s : SavedState) (macros : List _) (evalFns : List _) (failures : Array EvalTacticFailure) : TacticM Unit :=
match macros with
| [] => eval s evalFns failures
| m :: ms =>
try
withReader ({ · with elaborator := m.declName }) do
withTacticInfoContext stx do
let stx' ← adaptMacro m.value stx
evalTactic stx'
catch ex =>
if ms.isEmpty then throw ex -- (*)
s.restore; loop ms
loop macros
catch ex => handleEx s failures ex (expandEval s ms evalFns)
partial def expandTacticMacro (s : SavedState) (stx : Syntax) : TacticM Unit := do
expandTacticMacroFns s stx (macroAttribute.getEntries (← getEnv) stx.getKind)
partial def evalTacticAux (stx : Syntax) : TacticM Unit :=
withRef stx <| withIncRecDepth <| withFreshMacroScope <| match stx with
| .node _ k _ =>
if k == nullKind then
-- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]`
stx.getArgs.forM evalTactic
else do
trace[Elab.step] "{stx}"
let s ← Tactic.saveState
match tacticElabAttribute.getEntries (← getEnv) stx.getKind with
| [] => expandTacticMacro s stx
| evalFns => evalTacticUsing s stx evalFns
| .missing => pure ()
| _ => throwError m!"unexpected tactic{indentD stx}"
partial def evalTactic (stx : Syntax) : TacticM Unit :=
evalTacticAux stx
end
eval (s : SavedState) (evalFns : List _) (failures : Array EvalTacticFailure) : TacticM Unit := do
match evalFns with
| [] => throwExs failures
| evalFn::evalFns => do
try
withReader ({ · with elaborator := evalFn.declName }) <| withTacticInfoContext stx <| evalFn.value stx
catch ex => handleEx s failures ex (eval s evalFns)
def throwNoGoalsToBeSolved : TacticM α :=
throwError "no goals to be solved"

12
stage0/src/Lean/Elab/Tactic/ElabTerm.lean generated
View file

@ -242,14 +242,10 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId
match stx with
| `(tactic| rename $typeStx:term => $h:ident) => do
withMainContext do
/- Remark: we must not use `withoutModifyingState` because we may miss errors message.
For example, suppose the following `elabTerm` logs an error during elaboration.
In this scenario, the term `type` contains a synthetic `sorry`, and the error
message `"failed to find ..."` is not logged by the outer loop.
By using `withoutModifyingStateWithInfoAndMessages`, we ensure that
the messages and the info trees are preserved while the rest of the
state is backtracked. -/
let fvarId ← withoutModifyingStateWithInfoAndMessages <| withNewMCtxDepth do
/- Remark: we also use `withoutRecover` to make sure `elabTerm` does not succeed
using `sorryAx`, and we get `"failed to find ..."` which will not be logged because
it contains synthetic sorry's -/
let fvarId ← withoutModifyingState <| withNewMCtxDepth <| withoutRecover do
let type ← elabTerm typeStx none (mayPostpone := true)
let fvarId? ← (← getLCtx).findDeclRevM? fun localDecl => do
if (← isDefEq type localDecl.type) then return localDecl.fvarId else return none

14
stage0/src/Lean/Elab/Term.lean generated
View file

@ -850,13 +850,13 @@ Otherwise, we just use the basic `tryCoe`.
Extensions for monads.
1- Try to unify `n` and `m`. If it succeeds, then we use
```
coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β
```
`n` must be a `Monad` to use this one.
1. Try to unify `n` and `m`. If it succeeds, then we use
```
coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β
```
`n` must be a `Monad` to use this one.
2- If there is monad lift from `m` to `n` and we can unify `α` and `β`, we use
2. If there is monad lift from `m` to `n` and we can unify `α` and `β`, we use
```
liftM : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [self : MonadLiftT m n] {α : Type u_1}, m α → n α
```
@ -871,7 +871,7 @@ Extensions for monads.
```
3- If there is a monad lif from `m` to `n` and a coercion from `α` to `β`, we use
3. If there is a monad lif from `m` to `n` and a coercion from `α` to `β`, we use
```
liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β
```

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

@ -732,9 +732,6 @@ opaque eqv (a : @& Expr) (b : @& Expr) : Bool
instance : BEq Expr where
beq := Expr.eqv
protected unsafe def ptrEq (a b : Expr) : Bool :=
ptrAddrUnsafe a == ptrAddrUnsafe b
/--
Return true iff `a` and `b` are equal.
Binder names and annotations are taking into account.
@ -1393,101 +1390,120 @@ def containsFVar (e : Expr) (fvarId : FVarId) : Bool :=
e.hasAnyFVar (· == fvarId)
/-!
The update functions here are defined using C code. They will try to avoid
allocating new values using pointer equality.
The hypotheses `(h : e.is...)` are used to ensure Lean will not crash
at runtime.
The `update*!` functions are inlined and provide a convenient way of using the
update proofs without providing proofs.
Note that if they are used under a match-expression, the compiler will eliminate
the double-match.
The update functions try to avoid allocating new values using pointer equality.
Note that if the `update*!` functions are used under a match-expression,
the compiler will eliminate the double-match.
-/
@[extern "lean_expr_update_app"]
def updateApp (e : Expr) (newFn : Expr) (newArg : Expr) (h : e.isApp) : Expr :=
mkApp newFn newArg
@[inline] def updateApp! (e : Expr) (newFn : Expr) (newArg : Expr) : Expr :=
match h : e with
| app .. => updateApp e newFn newArg (h ▸ rfl)
| _ => panic! "application expected"
@[extern "lean_expr_update_const"]
def updateConst (e : Expr) (newLevels : List Level) (h : e.isConst) : Expr :=
mkConst e.constName! newLevels
@[inline] def updateConst! (e : Expr) (newLevels : List Level) : Expr :=
match h : e with
| const .. => updateConst e newLevels (h ▸ rfl)
| _ => panic! "constant expected"
@[extern "lean_expr_update_sort"]
def updateSort (e : Expr) (newLevel : Level) (h : e.isSort) : Expr :=
mkSort newLevel
@[inline] def updateSort! (e : Expr) (newLevel : Level) : Expr :=
match h : e with
| sort .. => updateSort e newLevel (h ▸ rfl)
| _ => panic! "level expected"
@[extern "lean_expr_update_proj"]
def updateProj (e : Expr) (newExpr : Expr) (h : e.isProj) : Expr :=
@[inline] private unsafe def updateApp!Impl (e : Expr) (newFn : Expr) (newArg : Expr) : Expr :=
match e with
| proj s i .. => mkProj s i newExpr
| _ => e -- unreachable because of `h`
| app fn arg => if ptrEq fn newFn && ptrEq arg newArg then e else mkApp newFn newArg
| _ => panic! "application expected"
@[extern "lean_expr_update_mdata"]
def updateMData (e : Expr) (newExpr : Expr) (h : e.isMData) : Expr :=
@[implementedBy updateApp!Impl]
def updateApp! (e : Expr) (newFn : Expr) (newArg : Expr) : Expr :=
match e with
| mdata d .. => mkMData d newExpr
| _ => e -- unreachable because of `h`
| app _ _ => mkApp newFn newArg
| _ => panic! "application expected"
@[inline] def updateMData! (e : Expr) (newExpr : Expr) : Expr :=
match h : e with
| mdata .. => updateMData e newExpr (h ▸ rfl)
| _ => panic! "mdata expected"
@[inline] private unsafe def updateConst!Impl (e : Expr) (newLevels : List Level) : Expr :=
match e with
| const n ls => if ptrEqList ls newLevels then e else mkConst n newLevels
| _ => panic! "constant expected"
@[inline] def updateProj! (e : Expr) (newExpr : Expr) : Expr :=
match h : e with
| proj .. => updateProj e newExpr (h ▸ rfl)
| _ => panic! "proj expected"
@[implementedBy updateConst!Impl]
def updateConst! (e : Expr) (newLevels : List Level) : Expr :=
match e with
| const n _ => mkConst n newLevels
| _ => panic! "constant expected"
@[extern "lean_expr_update_forall"]
def updateForall (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) (h : e.isForall) : Expr :=
mkForall e.bindingName! newBinfo newDomain newBody
@[inline] private unsafe def updateSort!Impl (e : Expr) (u' : Level) : Expr :=
match e with
| sort u => if ptrEq u u' then e else mkSort u'
| _ => panic! "level expected"
@[inline] def updateForall! (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) : Expr :=
match h : e with
| forallE .. => updateForall e newBinfo newDomain newBody (h ▸ rfl)
| _ => panic! "forall expected"
@[implementedBy updateSort!Impl]
def updateSort! (e : Expr) (newLevel : Level) : Expr :=
match e with
| sort _ => mkSort newLevel
| _ => panic! "level expected"
@[inline] def updateForallE! (e : Expr) (newDomain : Expr) (newBody : Expr) : Expr :=
match h : e with
| forallE _ _ _ c => updateForall e c newDomain newBody (h ▸ rfl)
@[inline] private unsafe def updateMData!Impl (e : Expr) (newExpr : Expr) : Expr :=
match e with
| mdata d a => if ptrEq a newExpr then e else mkMData d newExpr
| _ => panic! "mdata expected"
@[implementedBy updateMData!Impl]
def updateMData! (e : Expr) (newExpr : Expr) : Expr :=
match e with
| mdata d _ => mkMData d newExpr
| _ => panic! "mdata expected"
@[inline] private unsafe def updateProj!Impl (e : Expr) (newExpr : Expr) : Expr :=
match e with
| proj s i a => if ptrEq a newExpr then e else mkProj s i newExpr
| _ => panic! "proj expected"
@[implementedBy updateProj!Impl]
def updateProj! (e : Expr) (newExpr : Expr) : Expr :=
match e with
| proj s i _ => mkProj s i newExpr
| _ => panic! "proj expected"
@[inline] private unsafe def updateForall!Impl (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) : Expr :=
match e with
| forallE n d b bi =>
if ptrEq d newDomain && ptrEq b newBody && bi == newBinfo then
e
else
mkForall n newBinfo newDomain newBody
| _ => panic! "forall expected"
@[extern "lean_expr_update_lambda"]
def updateLambda (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) (h : e.isLambda) : Expr :=
mkLambda e.bindingName! newBinfo newDomain newBody
@[implementedBy updateForall!Impl]
def updateForall! (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) : Expr :=
match e with
| forallE n _ _ _ => mkForall n newBinfo newDomain newBody
| _ => panic! "forall expected"
@[inline] def updateLambda! (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) : Expr :=
match h : e with
| lam .. => updateLambda e newBinfo newDomain newBody (h ▸ rfl)
| _ => panic! "lambda expected"
@[inline] def updateForallE! (e : Expr) (newDomain : Expr) (newBody : Expr) : Expr :=
match e with
| forallE n d b bi => updateForall! (forallE n d b bi) bi newDomain newBody
| _ => panic! "forall expected"
@[inline] def updateLambdaE! (e : Expr) (newDomain : Expr) (newBody : Expr) : Expr :=
match h : e with
| lam _ _ _ c => updateLambda e c newDomain newBody (h ▸ rfl)
@[inline] private unsafe def updateLambda!Impl (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) : Expr :=
match e with
| lam n d b bi =>
if ptrEq d newDomain && ptrEq b newBody && bi == newBinfo then
e
else
mkLambda n newBinfo newDomain newBody
| _ => panic! "lambda expected"
@[extern "lean_expr_update_let"]
def updateLet (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) (h : e.isLet) : Expr :=
mkLet e.letName! newType newVal newBody
@[implementedBy updateLambda!Impl]
def updateLambda! (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) : Expr :=
match e with
| lam n _ _ _ => mkLambda n newBinfo newDomain newBody
| _ => panic! "lambda expected"
@[inline] def updateLet! (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) : Expr :=
match h : e with
| letE .. => updateLet e newType newVal newBody (h ▸ rfl)
| _ => panic! "let expression expected"
@[inline] def updateLambdaE! (e : Expr) (newDomain : Expr) (newBody : Expr) : Expr :=
match e with
| lam n d b bi => updateLambda! (lam n d b bi) bi newDomain newBody
| _ => panic! "lambda expected"
@[inline] private unsafe def updateLet!Impl (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) : Expr :=
match e with
| letE n t v b nonDep =>
if ptrEq t newType && ptrEq v newVal && ptrEq b newBody then
e
else
letE n newType newVal newBody nonDep
| _ => panic! "let expression expected"
@[implementedBy updateLet!Impl]
def updateLet! (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) : Expr :=
match e with
| letE n _ _ _ c => letE n newType newVal newBody c
| _ => panic! "let expression expected"
def updateFn : Expr → Expr → Expr
| e@(app f a), g => e.updateApp! (updateFn f g) a

65
stage0/src/Lean/Level.lean generated
View file

@ -493,11 +493,9 @@ end Level
elseK ()
/- Similar to `mkLevelMax`, but applies cheap simplifications -/
@[export lean_level_mk_max_simp]
def mkLevelMax' (u v : Level) : Level :=
mkLevelMaxCore u v fun _ => mkLevelMax u v
@[export lean_level_simp_max]
def simpLevelMax' (u v : Level) (d : Level) : Level :=
mkLevelMaxCore u v fun _ => d
@ -509,51 +507,52 @@ def simpLevelMax' (u v : Level) (d : Level) : Level :=
else elseK ()
/- Similar to `mkLevelIMax`, but applies cheap simplifications -/
@[export lean_level_mk_imax_simp]
def mkLevelIMax' (u v : Level) : Level :=
mkLevelIMaxCore u v fun _ => mkLevelIMax u v
@[export lean_level_simp_imax]
def simpLevelIMax' (u v : Level) (d : Level) :=
mkLevelIMaxCore u v fun _ => d
namespace Level
/- The update functions here are defined using C code. They will try to avoid
allocating new values using pointer equality.
The hypotheses `(h : e.is...)` are used to ensure Lean will not crash
at runtime.
The `update*!` functions are inlined and provide a convenient way of using the
update proofs without providing proofs.
Note that if they are used under a match-expression, the compiler will eliminate
the double-match. -/
/-!
The update functions try to avoid allocating new values using pointer equality.
Note that if the `update*!` functions are used under a match-expression,
the compiler will eliminate the double-match.
-/
@[extern "lean_level_update_succ"]
def updateSucc (lvl : Level) (newLvl : Level) (h : lvl.isSucc) : Level :=
mkLevelSucc newLvl
@[inline] private unsafe def updateSucc!Impl (lvl : Level) (newLvl : Level) : Level :=
match lvl with
| succ l => if ptrEq l newLvl then lvl else mkLevelSucc newLvl
| _ => panic! "succ level expected"
@[inline] def updateSucc! (lvl : Level) (newLvl : Level) : Level :=
match h : lvl with
| succ .. => updateSucc lvl newLvl (h ▸ rfl)
| _ => panic! "succ level expected"
@[implementedBy updateSucc!Impl]
def updateSucc! (lvl : Level) (newLvl : Level) : Level :=
match lvl with
| succ _ => mkLevelSucc newLvl
| _ => panic! "succ level expected"
@[extern "lean_level_update_max"]
def updateMax (lvl : Level) (newLhs : Level) (newRhs : Level) (h : lvl.isMax) : Level :=
mkLevelMax' newLhs newRhs
@[inline] private unsafe def updateMax!Impl (lvl : Level) (newLhs : Level) (newRhs : Level) : Level :=
match lvl with
| max lhs rhs => if ptrEq lhs newLhs && ptrEq rhs newRhs then simpLevelMax' newLhs newRhs lvl else mkLevelMax' newLhs newRhs
| _ => panic! "max level expected"
@[inline] def updateMax! (lvl : Level) (newLhs : Level) (newRhs : Level) : Level :=
match h : lvl with
| max .. => updateMax lvl newLhs newRhs (h ▸ rfl)
| _ => panic! "max level expected"
@[implementedBy updateMax!Impl]
def updateMax! (lvl : Level) (newLhs : Level) (newRhs : Level) : Level :=
match lvl with
| max _ _ => mkLevelMax' newLhs newRhs
| _ => panic! "max level expected"
@[extern "lean_level_update_imax"]
def updateIMax (lvl : Level) (newLhs : Level) (newRhs : Level) (h : lvl.isIMax) : Level :=
mkLevelIMax' newLhs newRhs
@[inline] private unsafe def updateIMax!Impl (lvl : Level) (newLhs : Level) (newRhs : Level) : Level :=
match lvl with
| imax lhs rhs => if ptrEq lhs newLhs && ptrEq rhs newRhs then simpLevelIMax' newLhs newRhs lvl else mkLevelIMax' newLhs newRhs
| _ => panic! "imax level expected"
@[inline] def updateIMax! (lvl : Level) (newLhs : Level) (newRhs : Level) : Level :=
match h : lvl with
| imax .. => updateIMax lvl newLhs newRhs (h ▸ rfl)
| _ => panic! "imax level expected"
@[implementedBy updateIMax!Impl]
def updateIMax! (lvl : Level) (newLhs : Level) (newRhs : Level) : Level :=
match lvl with
| imax _ _ => mkLevelIMax' newLhs newRhs
| _ => panic! "imax level expected"
def mkNaryMax : List Level → Level
| [] => levelZero

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

@ -188,18 +188,18 @@ private def processAsPattern (p : Problem) : MetaM Problem :=
match alt.patterns with
| Pattern.as fvarId p h :: ps =>
/- We used to use `checkAndReplaceFVarId` here, but `x` and `fvarId` may have different types
when dependent types are beind used. Let's consider the repro for issue #471
```
inductive vec : Nat → Type
| nil : vec 0
| cons : Int → vec n → vec n.succ
when dependent types are beind used. Let's consider the repro for issue #471
```
inductive vec : Nat → Type
| nil : vec 0
| cons : Int → vec n → vec n.succ
def vec_len : vec n → Nat
| vec.nil => 0
| x@(vec.cons h t) => vec_len t + 1
def vec_len : vec n → Nat
| vec.nil => 0
| x@(vec.cons h t) => vec_len t + 1
```
we reach the state
```
we reach the state
```
[Meta.Match.match] remaining variables: [x✝:(vec n✝)]
alternatives:
@ -297,7 +297,7 @@ def assign (fvarId : FVarId) (v : Expr) : M Bool := do
The first step is a variable-transition which replaces `β` with `β✝` in the first and third alternatives.
The constraint `β✝ === α` in the second alternative is lost. Note that `α` is not an alternative variable.
After applying the variable-transition step twice, we reach the following state
``lean
```lean
[Meta.Match.match] remaining variables: [f✝:(Arrow β✝ γ✝), g✝:(Arrow α β✝)]
alternatives:
[g:(Arrow α β✝)] |- [(Arrow.id .(β✝)), g] => h_1 β✝ g

8
stage0/src/Lean/Meta/Tactic/Constructor.lean generated
View file

@ -9,7 +9,11 @@ import Lean.Meta.Tactic.Apply
namespace Lean.Meta
def constructor (mvarId : MVarId) : MetaM (List MVarId) := do
/--
When the goal `mvarId` is an inductive datatype,
`constructor` calls `apply` with the first matching constructor.
-/
def constructor (mvarId : MVarId) (cfg : ApplyConfig := {}) : MetaM (List MVarId) := do
withMVarContext mvarId do
checkNotAssigned mvarId `constructor
let target ← getMVarType' mvarId
@ -18,7 +22,7 @@ def constructor (mvarId : MVarId) : MetaM (List MVarId) := do
fun ival us => do
for ctor in ival.ctors do
try
return ← apply mvarId (Lean.mkConst ctor us)
return ← apply mvarId (Lean.mkConst ctor us) cfg
catch _ =>
pure ()
throwTacticEx `constructor mvarId "no applicable constructor found"

4
stage0/src/Lean/Parser/Command.lean generated
View file

@ -132,8 +132,8 @@ def openDecl := openHiding <|> openRenaming <|> openOnly <|> openSimple
@[builtinCommandParser] def «open» := leading_parser withPosition ("open " >> openDecl)
@[builtinCommandParser] def «mutual» := leading_parser "mutual " >> many1 (ppLine >> notSymbol "end" >> commandParser) >> ppDedent (ppLine >> "end") >> terminationSuffix
@[builtinCommandParser] def «initialize» := leading_parser optional visibility >> "initialize " >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
@[builtinCommandParser] def «builtin_initialize» := leading_parser optional visibility >> "builtin_initialize " >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
def initializeKeyword := leading_parser "initialize " <|> "builtin_initialize "
@[builtinCommandParser] def «initialize» := leading_parser declModifiers false >> initializeKeyword >> optional (atomic (ident >> Term.typeSpec >> Term.leftArrow)) >> Term.doSeq
@[builtinCommandParser] def «in» := trailing_parser withOpen (" in " >> commandParser)

16
stage0/src/Lean/Server/FileWorker/RequestHandling.lean generated
View file

@ -237,18 +237,10 @@ open Parser.Command in
partial def handleDocumentSymbol (_ : DocumentSymbolParams)
: RequestM (RequestTask DocumentSymbolResult) := do
let doc ← readDoc
mapTask (← doc.cmdSnaps.waitHead?) fun _ => do
let ⟨cmdSnaps, e?⟩ ← doc.cmdSnaps.getFinishedPrefix
let mut stxs := cmdSnaps.map (·.stx)
match e? with
| some ElabTaskError.aborted =>
throw RequestError.fileChanged
| some (ElabTaskError.ioError e) =>
throw (e : RequestError)
| _ => pure ()
let lastSnap := cmdSnaps.getLast! -- see `waitHead?` above
stxs := stxs ++ (← parseAhead doc.meta.mkInputContext lastSnap).toList
-- bad: we have to wait on elaboration of the entire file before we can report document symbols
let t ← doc.cmdSnaps.waitAll
mapTask t fun (snaps, _) => do
let mut stxs := snaps.map (·.stx)
let (syms, _) := toDocumentSymbols doc.meta.text stxs
return { syms := syms.toArray }
where

5
stage0/src/Lean/Server/Rpc/Basic.lean generated
View file

@ -42,10 +42,13 @@ non-JSON-serializable fields can be auto-encoded in two ways:
-- TODO(WN): for Lean.js, have third parameter defining the client-side structure;
-- or, compile `WithRpcRef` to "opaque reference" on the client
class RpcEncoding (α : Type) (β : outParam Type) where
rpcEncode {m : Type → Type} [Monad m] [MonadRpcSession m] : α → m β
rpcEncode {m : Type → Type} [Monad m] [MonadRpcSession m] : α → ExceptT String m β
rpcDecode {m : Type → Type} [Monad m] [MonadRpcSession m] : β → ExceptT String m α
export RpcEncoding (rpcEncode rpcDecode)
instance : Nonempty (RpcEncoding α β) :=
⟨{ rpcEncode := fun _ => throw "unreachable", rpcDecode := fun _ => throw "unreachable" }⟩
instance [FromJson α] [ToJson α] : RpcEncoding α α where
rpcEncode := pure
rpcDecode := pure

262
stage0/src/Lean/Server/Rpc/Deriving.lean generated
View file

@ -20,26 +20,14 @@ private def deriveWithRefInstance (typeNm : Name) : CommandElabM Bool := do
-- TODO(WN): check that `typeNm` is not a scalar type
let typeId := mkIdent typeNm
let cmds ← `(
section
variable {m : Type → Type}
unsafe def encodeUnsafe [Monad m] [MonadRpcSession m] (r : WithRpcRef $typeId:ident) : m Lsp.RpcRef :=
WithRpcRef.encodeUnsafe $(quote typeNm) r
unsafe def unsafeInst : RpcEncoding (WithRpcRef $typeId:ident) Lsp.RpcRef where
rpcEncode := WithRpcRef.encodeUnsafe $(quote typeNm)
rpcDecode := WithRpcRef.decodeUnsafeAs $typeId:ident $(quote typeNm)
@[implementedBy encodeUnsafe]
opaque encode [Monad m] [MonadRpcSession m] (r : WithRpcRef $typeId:ident) : m Lsp.RpcRef :=
pure ⟨0⟩
@[implementedBy unsafeInst]
opaque inst : RpcEncoding (WithRpcRef $typeId) Lsp.RpcRef
unsafe def decodeUnsafe [Monad m] [MonadRpcSession m] (r : Lsp.RpcRef) : ExceptT String m (WithRpcRef $typeId:ident) :=
WithRpcRef.decodeUnsafeAs $typeId:ident $(quote typeNm) r
@[implementedBy decodeUnsafe]
opaque decode [Monad m] [MonadRpcSession m] (r : Lsp.RpcRef) : ExceptT String m (WithRpcRef $typeId:ident) :=
throw "unreachable"
instance : RpcEncoding (WithRpcRef $typeId:ident) Lsp.RpcRef :=
{ rpcEncode := encode
rpcDecode := decode }
end
instance : RpcEncoding (WithRpcRef $typeId) Lsp.RpcRef := inst
)
elabCommand cmds
return true
@ -85,45 +73,27 @@ def withFieldsFlattened (indVal : InductiveVal) (params : Array Expr)
end
def isOptField (n : Name) : Bool :=
n.toString.endsWith "?"
private def getRpcPacketFor (ty : Expr) : MetaM Expr := do
let packetTy ← mkFreshExprMVar (Expr.sort levelOne)
let _ ← synthInstance (mkApp2 (mkConst ``RpcEncoding) ty packetTy)
instantiateMVars packetTy
private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr) : TermElabM Command :=
private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr)
(paramBinders packetParamBinders encInstBinders : Array (TSyntax ``Parser.Term.bracketedBinder)) : TermElabM Command := do
withFields indVal params fun fields => do
trace[Elab.Deriving.RpcEncoding] "for structure {indVal.name} with params {params}"
-- Postulate that every field have a rpc encoding, storing the encoding type ident
-- in `fieldEncIds`. When multiple fields have the same type, we reuse the encoding type
-- as otherwise typeclass synthesis fails.
let mut binders := #[]
let mut fieldIds := #[]
let mut fieldEncIds : Array Term := #[]
let mut uniqFieldEncIds : Array Ident := #[]
let mut fieldEncIds' : DiscrTree Ident := {}
let mut fieldEncTypeStxs := #[]
for (fieldName, fieldTp) in fields do
let mut fieldTp := fieldTp
if isOptField fieldName then
if !fieldTp.isAppOf ``Option then
throwError "optional field '{fieldName}' has type{indentD m!"{fieldTp}"}\nbut is expected to have type{indentD "Option _"}" --"
fieldTp := fieldTp.getArg! 0
-- postulate that the field has an encoding and remember the encoding's binder name
let fieldEncTypeStx ← PrettyPrinter.delab (← getRpcPacketFor fieldTp)
let stx ← PrettyPrinter.delab fieldTp
fieldIds := fieldIds.push <| mkIdent fieldName
let mut fieldEncId : Ident := ⟨Syntax.missing⟩
match (← fieldEncIds'.getMatch fieldTp).back? with
| none =>
fieldEncId ← mkIdent <$> mkFreshUserName fieldName
binders := binders.push (← `(bracketedBinder| ( $fieldEncId:ident )))
let stx ← PrettyPrinter.delab fieldTp
binders := binders.push
(← `(bracketedBinder| [ $(mkIdent ``Lean.Server.RpcEncoding) $stx $fieldEncId:ident ]))
fieldEncIds' ← fieldEncIds'.insert fieldTp fieldEncId
uniqFieldEncIds := uniqFieldEncIds.push fieldEncId
| some fid => fieldEncId := fid
if isOptField fieldName then
fieldEncIds := fieldEncIds.push <| ← ``(Option $fieldEncId:ident)
else
fieldEncIds := fieldEncIds.push fieldEncId
fieldEncTypeStxs := fieldEncTypeStxs.push fieldEncTypeStx
binders := binders.push
(← `(bracketedBinder| [ RpcEncoding $stx $fieldEncTypeStx ]))
-- helpers for field initialization syntax
let fieldInits (func : Name) := fieldIds.mapM fun fid =>
@ -134,115 +104,88 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
-- helpers for type name syntax
let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
let typeId := Syntax.mkApp (← `(@$(mkIdent indVal.name))) paramIds
let packetId ← mkIdent <$> mkFreshUserName `RpcEncodingPacket
let packetAppliedId := Syntax.mkApp packetId uniqFieldEncIds
let instId := mkIdent (`_root_ ++ indVal.name.appendBefore "instRpcEncoding")
`(variable $binders*
`(variable $packetParamBinders* in
structure RpcEncodingPacket where
$[($fieldIds : $fieldEncTypeStxs)]*
deriving FromJson, ToJson
structure $packetId:ident where
$[($fieldIds : $fieldEncIds)]*
deriving $(mkIdent ``FromJson), $(mkIdent ``ToJson)
instance : $(mkIdent ``RpcEncoding) $typeId $packetAppliedId where
rpcEncode a := return {
$[$encInits],*
}
rpcDecode a := return {
$[$decInits],*
}
variable $(paramBinders ++ packetParamBinders ++ encInstBinders)* in
@[instance] def $instId := show RpcEncoding $typeId (RpcEncodingPacket ..) from {
rpcEncode := fun a => return { $[$encInits],* }
rpcDecode := fun a => return { $[$decInits],* }
}
)
private structure CtorState where
-- names of encoded argument types in the RPC packet
encArgTypes : DiscrTree Name := {}
uniqEncArgTypes : Array Name := #[]
-- binders for `encArgTypes` as well as the relevant `RpcEncoding`s
binders : Array (TSyntax ``Parser.Term.bracketedBinder) := #[]
-- the syntax of each constructor in the packet
ctors : Array (TSyntax ``Parser.Command.ctor) := #[]
-- syntax of each arm of the `rpcEncode` pattern-match
encodes : Array (TSyntax ``Parser.Term.matchAlt) := #[]
-- syntax of each arm of the `rpcDecode` pattern-match
decodes : Array (TSyntax ``Parser.Term.matchAlt) := #[]
deriving Inhabited
private def matchF := Lean.Parser.Term.matchAlt (rhsParser := Lean.Parser.termParser)
private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr) : TermElabM Command := do
private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr)
(paramBinders packetParamBinders encInstBinders : Array (TSyntax ``Parser.Term.bracketedBinder)) : TermElabM Command := do
trace[Elab.Deriving.RpcEncoding] "for inductive {indVal.name} with params {params}"
withoutModifyingEnv do
let packetNm := (← `(RpcEncodingPacket)).1.getId
addDecl <| .axiomDecl {
name := packetNm
levelParams := []
type := mkSort levelOne
isUnsafe := true
}
let pktCtorTp := mkConst packetNm
let recInstTp := mkApp2 (mkConst ``RpcEncoding) (mkAppN (mkConst indVal.name) params) pktCtorTp
withLocalDecl `inst .instImplicit recInstTp fun _ => do
let st ← foldWithConstructors indVal params (init := { : CtorState }) fun acc ctor argVars _ => do
-- create the constructor
let fieldStxs ← argVars.mapM fun arg => do
let packetTp ← getRpcPacketFor (← inferType arg)
let tyStx ← PrettyPrinter.delab packetTp
let name := (← getFVarLocalDecl arg).userName
`(bracketedBinder| ($(mkIdent name) : $tyStx))
let pktCtor ← `(Parser.Command.ctor| | $(mkIdent ctor.getString!):ident $[$fieldStxs]* : RpcEncodingPacket)
-- produce all encoding types and binders for them
let st ← foldWithConstructors indVal params (init := { : CtorState}) fun acc ctor argVars tp => do
trace[Elab.Deriving.RpcEncoding] "{ctor} : {argVars} → {tp}"
let mut acc := acc
let argFVars ← argVars.mapM (LocalDecl.fvarId <$> getFVarLocalDecl ·)
for arg in argVars do
let argTp ← inferType arg
if (← findExprDependsOn argTp (pf := fun fv => argFVars.contains fv)) then
throwError "cross-argument dependencies are not supported ({arg} : {argTp})"
-- create encoder and decoder match arms
let nms ← argVars.mapM fun _ => mkIdent <$> mkFreshBinderName
let mkPattern (src : Name) := Syntax.mkApp (mkIdent <| Name.mkStr src ctor.getString!) nms
let mkBody (tgt : Name) (func : Name) : TermElabM Term := do
let items ← nms.mapM fun nm => `(← $(mkIdent func) $nm)
let tm := Syntax.mkApp (mkIdent <| Name.mkStr tgt ctor.getString!) items
`(return $tm:term)
if (← acc.encArgTypes.getMatch argTp).isEmpty then
let tid ← mkFreshUserName `_rpcEnc
let argTpStx ← PrettyPrinter.delab argTp
acc := { acc with encArgTypes := ← acc.encArgTypes.insert argTp tid
uniqEncArgTypes := acc.uniqEncArgTypes.push tid
binders := acc.binders.append #[
(← `(bracketedBinder| ( $(mkIdent tid):ident ))),
(← `(bracketedBinder| [ $(mkIdent ``Lean.Server.RpcEncoding) $argTpStx $(mkIdent tid):ident ]))
] }
return acc
let encArm ← `(matchF| | $(mkPattern indVal.name):term => $(← mkBody packetNm ``rpcEncode))
let decArm ← `(matchF| | $(mkPattern packetNm):term => $(← mkBody indVal.name ``rpcDecode))
-- introduce encoding types into the local context so that we can use the delaborator to print them
withLocalDecls
(st.uniqEncArgTypes.map fun tid => (tid, BinderInfo.default, fun _ => pure <| mkSort levelOne))
fun ts => do
trace[Elab.Deriving.RpcEncoding] m!"RpcEncoding type binders : {ts}"
return { acc with ctors := acc.ctors.push pktCtor
encodes := acc.encodes.push ⟨encArm⟩
decodes := acc.decodes.push ⟨decArm⟩ }
let packetNm ← mkFreshUserName `RpcEncodingPacket
let st ← foldWithConstructors indVal params (init := st) fun acc ctor argVars _ => do
-- create the constructor
let mut pktCtorTp := Lean.mkConst packetNm
for arg in argVars.reverse do
let argTp ← inferType arg
let encTpNm := (← acc.encArgTypes.getMatch argTp).back
let encTp ← elabTerm (mkIdent encTpNm) none
pktCtorTp := mkForall (← getFVarLocalDecl arg).userName BinderInfo.default encTp pktCtorTp
-- TODO(WN): this relies on delab printing non-macro-scoped user names in non-dependent foralls
-- to generate the expected JSON encoding
let pktCtorTpStx ← PrettyPrinter.delab pktCtorTp
let pktCtor ← `(Lean.Parser.Command.ctor| | $(mkIdent ctor.getString!):ident : $pktCtorTpStx:term)
-- helpers for type name syntax
let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
let typeId := Syntax.mkApp (← `(@$(mkIdent indVal.name))) paramIds
let instId := mkIdent (`_root_ ++ indVal.name.appendBefore "instRpcEncoding")
-- create encoder and decoder match arms
let nms ← argVars.mapM fun _ => mkIdent <$> mkFreshBinderName
let mkPattern (src : Name) := Syntax.mkApp (mkIdent <| Name.mkStr src ctor.getString!) nms
let mkBody (tgt : Name) (func : Name) : TermElabM Term := do
let items ← nms.mapM fun nm => `(← $(mkIdent func) $nm)
let tm := Syntax.mkApp (mkIdent <| Name.mkStr tgt ctor.getString!) items
`(return $tm:term)
`(variable $packetParamBinders:bracketedBinder* in
inductive RpcEncodingPacket where
$[$(st.ctors):ctor]*
deriving FromJson, ToJson
let encArm ← `(matchF| | $(mkPattern indVal.name):term => $(← mkBody packetNm ``rpcEncode))
let decArm ← `(matchF| | $(mkPattern packetNm):term => $(← mkBody indVal.name ``rpcDecode))
return { acc with ctors := acc.ctors.push pktCtor
encodes := acc.encodes.push ⟨encArm⟩
decodes := acc.decodes.push ⟨decArm⟩ }
-- helpers for type name syntax
let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
let typeId := Syntax.mkApp (← `(@$(mkIdent indVal.name))) paramIds
let packetAppliedId := Syntax.mkApp (mkIdent packetNm) (st.uniqEncArgTypes.map (mkIdent ·))
`(variable $st.binders*
inductive $(mkIdent packetNm) where
$[$(st.ctors):ctor]*
deriving $(mkIdent ``FromJson), $(mkIdent ``ToJson)
instance : $(mkIdent ``RpcEncoding) $typeId $packetAppliedId where
rpcEncode := fun x => match x with
$[$(st.encodes):matchAlt]*
rpcDecode := fun x => match x with
$[$(st.decodes):matchAlt]*
)
variable $(paramBinders ++ packetParamBinders ++ encInstBinders)* in
@[instance] partial def $instId := show RpcEncoding $typeId (RpcEncodingPacket ..) from
{ rpcEncode, rpcDecode }
where
rpcEncode {m} [Monad m] [MonadRpcSession m] (x : $typeId) : ExceptT String m (RpcEncodingPacket ..) :=
have inst : RpcEncoding $typeId (RpcEncodingPacket ..) := { rpcEncode, rpcDecode }
match x with $[$(st.encodes):matchAlt]*
rpcDecode {m} [Monad m] [MonadRpcSession m] (x : RpcEncodingPacket ..) : ExceptT String m $typeId :=
have inst : RpcEncoding $typeId (RpcEncodingPacket ..) := { rpcEncode, rpcDecode }
match x with $[$(st.decodes):matchAlt]*
)
/-- Creates an `RpcEncodingPacket` for `typeName`. For structures, the packet is a structure
with the same field names. For inductives, it mirrors the inductive structure with every field
@ -255,33 +198,35 @@ private def deriveInstance (typeName : Name) : CommandElabM Bool := do
if indVal.numIndices ≠ 0 then
throwError "indexed inductive families are not supported"
let cmds ← liftTermElabM none <|
let (paramBinders, packetParamBinders, encInstBinders) ← liftTermElabM none do
-- introduce fvars for all the parameters
forallTelescopeReducing indVal.type fun params _ => do
assert! params.size == indVal.numParams
let mut paramBinders := #[] -- input parameters
let mut packetParamBinders := #[] -- RPC encoding packets for type input parameters
let mut encInstBinders := #[] -- RPC encoding instance binders corresponding to packetParamBinders
-- bind every parameter and *some* (not named) `RpcEncoding` for it
let mut binders := #[]
for param in params do
let paramNm := (←getFVarLocalDecl param).userName
binders := binders.push (← `(bracketedBinder| ( $(mkIdent paramNm) )))
let paramNm := (← getFVarLocalDecl param).userName
let ty ← PrettyPrinter.delab (← inferType param)
paramBinders := paramBinders.push (← `(bracketedBinder| ($(mkIdent paramNm) : $ty)))
let packet := mkIdent (← mkFreshUserName (paramNm.appendAfter "Packet"))
-- only look for encodings for `Type` parameters
if !(← inferType param).isType then continue
binders := binders.push
(← `(bracketedBinder| [ $(mkIdent ``Lean.Server.RpcEncoding) $(mkIdent paramNm) _ ]))
return #[
← `(section),
← `(variable $binders*),
← if isStructure (← getEnv) typeName then
deriveStructureInstance indVal params
if (← inferType param).isType then
packetParamBinders := packetParamBinders.push (← `(bracketedBinder| ($packet : Type)))
encInstBinders := encInstBinders.push (← `(bracketedBinder| [RpcEncoding $(mkIdent paramNm) $packet]))
else
deriveInductiveInstance indVal params,
← `(end)
]
packetParamBinders := packetParamBinders.push paramBinders.back
return (paramBinders, packetParamBinders, encInstBinders)
elabCommand <| ← liftTermElabM none do
Term.elabBinders (paramBinders ++ packetParamBinders ++ encInstBinders) fun locals => do
let params := locals[:paramBinders.size]
if isStructure (← getEnv) typeName then
deriveStructureInstance indVal params paramBinders packetParamBinders encInstBinders
else
deriveInductiveInstance indVal params paramBinders packetParamBinders encInstBinders
for cmd in cmds do
elabCommand cmd.raw
return true
private unsafe def dispatchDeriveInstanceUnsafe (declNames : Array Name) (args? : Option (TSyntax ``Parser.Term.structInst)) : CommandElabM Bool := do
@ -289,8 +234,7 @@ private unsafe def dispatchDeriveInstanceUnsafe (declNames : Array Name) (args?
return false
let args ←
if let some args := args? then
let n ← liftCoreM <| mkFreshUserName `_args
liftTermElabM (some n) do
liftTermElabM none do
let argsT := mkConst ``DerivingParams
let args ← elabTerm args argsT
evalExpr' DerivingParams ``DerivingParams args

14
stage0/src/Lean/Server/Rpc/RequestHandling.lean generated
View file

@ -82,8 +82,18 @@ def wrapRpcProcedure (method : Name) paramType respType
RequestM.mapTask t fun
| Except.error e => throw e
| Except.ok ret => do
let act := rpcEncode (α := respType) (β := respLspType) (m := StateM FileWorker.RpcSession) ret
return toJson (← seshRef.modifyGet act.run)⟩
let act : StateM FileWorker.RpcSession (Except String respLspType) := do
let s ← get
match ← rpcEncode (α := respType) (β := respLspType) (m := StateM FileWorker.RpcSession) ret with
| .ok x => return .ok x
| .error e => set s; return .error e
match ← seshRef.modifyGet act.run with
| .ok x => return toJson x
| .error e =>
throwThe RequestError {
code := JsonRpc.ErrorCode.invalidParams
message := s!"Cannot encode result of RPC call '{method}'\n{e}"
}⟩
def registerBuiltinRpcProcedure (method : Name) paramType respType
{paramLspType} [RpcEncoding paramType paramLspType] [FromJson paramLspType]

16
stage0/src/Lean/Server/Snapshots.lean generated
View file

@ -83,22 +83,6 @@ def parseNextCmd (inputCtx : Parser.InputContext) (snap : Snapshot) : IO Syntax
Parser.parseCommand inputCtx pmctx snap.mpState snap.msgLog
return cmdStx
/--
Parse remaining file without elaboration. NOTE that doing so can lead to parse errors or even wrong syntax objects,
so it should only be done for reporting preliminary results! -/
partial def parseAhead (inputCtx : Parser.InputContext) (snap : Snapshot) : IO (Array Syntax) := do
let cmdState := snap.cmdState
let scope := cmdState.scopes.head!
let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
go inputCtx pmctx snap.mpState #[]
where
go inputCtx pmctx cmdParserState stxs := do
let (cmdStx, cmdParserState, _) := Parser.parseCommand inputCtx pmctx cmdParserState snap.msgLog
if Parser.isEOI cmdStx || Parser.isExitCommand cmdStx then
return stxs.push cmdStx
else
go inputCtx pmctx cmdParserState (stxs.push cmdStx)
register_builtin_option server.stderrAsMessages : Bool := {
defValue := true
group := "server"

2
stage0/src/Lean/Server/Watchdog.lean generated
View file

@ -682,7 +682,7 @@ def mkLeanServerCapabilities : ServerCapabilities := {
semanticTokensProvider? := some {
legend := {
tokenTypes := SemanticTokenType.names
tokenModifiers := #[]
tokenModifiers := SemanticTokenModifier.names
}
full := true
range := true

4
stage0/src/Lean/Util/HasConstCache.lean generated
View file

@ -11,7 +11,7 @@ structure HasConstCache (declName : Name) where
cache : Std.HashMapImp Expr Bool := Std.mkHashMapImp
unsafe def HasConstCache.containsUnsafe (e : Expr) : StateM (HasConstCache declName) Bool := do
if let some r := (← get).cache.find? (beq := ⟨Expr.ptrEq⟩) e then
if let some r := (← get).cache.find? (beq := ⟨ptrEq⟩) e then
return r
else
match e with
@ -25,7 +25,7 @@ unsafe def HasConstCache.containsUnsafe (e : Expr) : StateM (HasConstCache declN
| _ => return false
where
cache (e : Expr) (r : Bool) : StateM (HasConstCache declName) Bool := do
modify fun ⟨cache⟩ => ⟨cache.insert (beq := ⟨Expr.ptrEq⟩) e r |>.1⟩
modify fun ⟨cache⟩ => ⟨cache.insert (beq := ⟨ptrEq⟩) e r |>.1⟩
return r
/--

91
stage0/src/kernel/expr.cpp generated
View file

@ -330,97 +330,6 @@ expr update_let(expr const & e, expr const & new_type, expr const & new_value, e
return e;
}
extern "C" LEAN_EXPORT object * lean_expr_update_mdata(obj_arg e, obj_arg new_expr) {
if (mdata_expr(TO_REF(expr, e)).raw() != new_expr) {
object * r = lean_expr_mk_mdata(mdata_data(TO_REF(expr, e)).to_obj_arg(), new_expr);
lean_dec_ref(e);
return r;
} else {
lean_dec_ref(new_expr);
return e;
}
}
extern "C" LEAN_EXPORT object * lean_expr_update_const(obj_arg e, obj_arg new_levels) {
if (const_levels(TO_REF(expr, e)).raw() != new_levels) {
object * r = lean_expr_mk_const(const_name(TO_REF(expr, e)).to_obj_arg(), new_levels);
lean_dec_ref(e);
return r;
} else {
lean_dec(new_levels);
return e;
}
}
extern "C" LEAN_EXPORT object * lean_expr_update_sort(obj_arg e, obj_arg new_level) {
if (sort_level(TO_REF(expr, e)).raw() != new_level) {
object * r = lean_expr_mk_sort(new_level);
lean_dec_ref(e);
return r;
} else {
lean_dec(new_level);
return e;
}
}
extern "C" LEAN_EXPORT object * lean_expr_update_proj(obj_arg e, obj_arg new_expr) {
if (proj_expr(TO_REF(expr, e)).raw() != new_expr) {
object * r = lean_expr_mk_proj(proj_sname(TO_REF(expr, e)).to_obj_arg(), proj_idx(TO_REF(expr, e)).to_obj_arg(), new_expr);
lean_dec_ref(e);
return r;
} else {
lean_dec_ref(new_expr);
return e;
}
}
extern "C" LEAN_EXPORT object * lean_expr_update_app(obj_arg e, obj_arg new_fn, obj_arg new_arg) {
if (app_fn(TO_REF(expr, e)).raw() != new_fn || app_arg(TO_REF(expr, e)).raw() != new_arg) {
object * r = lean_expr_mk_app(new_fn, new_arg);
lean_dec_ref(e);
return r;
} else {
lean_dec_ref(new_fn); lean_dec_ref(new_arg);
return e;
}
}
extern "C" LEAN_EXPORT object * lean_expr_update_forall(obj_arg e, uint8 new_binfo, obj_arg new_domain, obj_arg new_body) {
if (binding_domain(TO_REF(expr, e)).raw() != new_domain || binding_body(TO_REF(expr, e)).raw() != new_body ||
binding_info(TO_REF(expr, e)) != static_cast<binder_info>(new_binfo)) {
object * r = lean_expr_mk_forall(binding_name(TO_REF(expr, e)).to_obj_arg(), new_domain, new_body, new_binfo);
lean_dec_ref(e);
return r;
} else {
lean_dec_ref(new_domain); lean_dec_ref(new_body);
return e;
}
}
extern "C" LEAN_EXPORT object * lean_expr_update_lambda(obj_arg e, uint8 new_binfo, obj_arg new_domain, obj_arg new_body) {
if (binding_domain(TO_REF(expr, e)).raw() != new_domain || binding_body(TO_REF(expr, e)).raw() != new_body ||
binding_info(TO_REF(expr, e)) != static_cast<binder_info>(new_binfo)) {
object * r = lean_expr_mk_lambda(binding_name(TO_REF(expr, e)).to_obj_arg(), new_domain, new_body, new_binfo);
lean_dec_ref(e);
return r;
} else {
lean_dec_ref(new_domain); lean_dec_ref(new_body);
return e;
}
}
extern "C" LEAN_EXPORT object * lean_expr_update_let(obj_arg e, obj_arg new_type, obj_arg new_val, obj_arg new_body) {
if (let_type(TO_REF(expr, e)).raw() != new_type || let_value(TO_REF(expr, e)).raw() != new_val ||
let_body(TO_REF(expr, e)).raw() != new_body) {
object * r = lean_expr_mk_let(let_name(TO_REF(expr, e)).to_obj_arg(), new_type, new_val, new_body);
lean_dec_ref(e);
return r;
} else {
lean_dec_ref(new_type); lean_dec_ref(new_val); lean_dec_ref(new_body);
return e;
}
}
extern "C" object * lean_expr_consume_type_annotations(obj_arg e);
expr consume_type_annotations(expr const & e) { return expr(lean_expr_consume_type_annotations(e.to_obj_arg())); }

32
stage0/src/kernel/level.cpp generated
View file

@ -29,10 +29,6 @@ extern "C" object * lean_level_mk_mvar(obj_arg);
extern "C" object * lean_level_mk_param(obj_arg);
extern "C" object * lean_level_mk_max(obj_arg, obj_arg);
extern "C" object * lean_level_mk_imax(obj_arg, obj_arg);
extern "C" object * lean_level_mk_max_simp(obj_arg, obj_arg);
extern "C" object * lean_level_mk_imax_simp(obj_arg, obj_arg);
extern "C" object * lean_level_simp_max(obj_arg, obj_arg, obj_arg);
extern "C" object * lean_level_simp_imax(obj_arg, obj_arg, obj_arg);
level mk_succ(level const & l) { return level(lean_level_mk_succ(l.to_obj_arg())); }
level mk_max_core(level const & l1, level const & l2) { return level(lean_level_mk_max(l1.to_obj_arg(), l2.to_obj_arg())); }
@ -293,34 +289,6 @@ level update_max(level const & l, level const & new_lhs, level const & new_rhs)
return mk_imax(new_lhs, new_rhs);
}
extern "C" LEAN_EXPORT object * lean_level_update_succ(obj_arg l, obj_arg new_arg) {
if (succ_of(TO_REF(level, l)).raw() == new_arg) {
lean_dec(new_arg);
return l;
} else {
lean_dec_ref(l);
return lean_level_mk_succ(new_arg);
}
}
extern "C" LEAN_EXPORT object * lean_level_update_max(obj_arg l, obj_arg new_lhs, obj_arg new_rhs) {
if (max_lhs(TO_REF(level, l)).raw() == new_lhs && max_rhs(TO_REF(level, l)).raw() == new_rhs) {
return lean_level_simp_max(new_lhs, new_rhs, l);
} else {
lean_dec_ref(l);
return lean_level_mk_max_simp(new_lhs, new_rhs);
}
}
extern "C" LEAN_EXPORT object * lean_level_update_imax(obj_arg l, obj_arg new_lhs, obj_arg new_rhs) {
if (imax_lhs(TO_REF(level, l)).raw() == new_lhs && imax_rhs(TO_REF(level, l)).raw() == new_rhs) {
return lean_level_simp_imax(new_lhs, new_rhs, l);
} else {
lean_dec_ref(l);
return lean_level_mk_imax_simp(new_lhs, new_rhs);
}
}
level instantiate(level const & l, names const & ps, levels const & ls) {
lean_assert(length(ps) == length(ls));
return replace(l, [=](level const & l) {

2
stage0/src/stdlib_flags.h generated
View file

@ -8,7 +8,7 @@ options get_default_options() {
// switch to `true` for ABI-breaking changes affecting meta code
opts = opts.update({"interpreter", "prefer_native"}, false);
// switch to `true` for changing built-in parsers used in quotations
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
opts = opts.update({"pp", "rawOnError"}, true);
#endif
return opts;

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

File diff suppressed because it is too large Load diff

2
stage0/stdlib/Init/NotationExtra.c generated
View file

@ -2153,7 +2153,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_expandExplicitBindersAux_loop___closed__13;
x_2 = l_Lean_expandExplicitBindersAux_loop___closed__14;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Lean_expandExplicitBindersAux_loop___closed__15;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

108
stage0/stdlib/Init/Util.c generated
View file

@ -41,6 +41,7 @@ lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at___aux__Init__Notation______ma
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
static lean_object* l___aux__Init__Util______macroRules__term_____x5b___x5d___x3f__1___closed__2;
LEAN_EXPORT uint8_t l_ptrEqList___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_withPtrEqDecEq___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_string_utf8_byte_size(lean_object*);
static lean_object* l___aux__Init__Util______macroRules__term_____x5b___x5d___x3f__1___closed__9;
@ -103,13 +104,18 @@ static lean_object* l_getElem_x21___rarg___closed__4;
LEAN_EXPORT lean_object* l_panicWithPos(lean_object*);
LEAN_EXPORT lean_object* l_panicWithPosWithDecl(lean_object*);
LEAN_EXPORT lean_object* l___aux__Init__Util______macroRules__term_____x5b___x5d___x21__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ptrEqList(lean_object*);
LEAN_EXPORT lean_object* l_ptrEq(lean_object*);
LEAN_EXPORT lean_object* l_panicWithPosWithDecl___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_ptrEqList___rarg___boxed(lean_object*, lean_object*);
lean_object* l_panic___rarg(lean_object*, lean_object*);
static lean_object* l___aux__Init__Util______macroRules__term_____x5b___x5d___x3f__1___closed__7;
static lean_object* l_term_____x5b___x5d___x3f___closed__19;
LEAN_EXPORT lean_object* l_getElem_x3f___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl___closed__1;
LEAN_EXPORT uint8_t l_ptrEq___rarg(lean_object*, lean_object*);
static lean_object* l_term_____x5b___x5d___x3f___closed__14;
LEAN_EXPORT lean_object* l_ptrEq___rarg___boxed(lean_object*, lean_object*);
static lean_object* l_term_____x5b___x5d___x3f___closed__22;
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_getElem_x3f(lean_object*, lean_object*, lean_object*, lean_object*);
@ -380,6 +386,106 @@ lean_dec(x_1);
return x_4;
}
}
LEAN_EXPORT uint8_t l_ptrEq___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
size_t x_3; size_t x_4; uint8_t x_5;
x_3 = lean_ptr_addr(x_1);
x_4 = lean_ptr_addr(x_2);
x_5 = lean_usize_dec_eq(x_3, x_4);
return x_5;
}
}
LEAN_EXPORT lean_object* l_ptrEq(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_ptrEq___rarg___boxed), 2, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_ptrEq___rarg___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_ptrEq___rarg(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT uint8_t l_ptrEqList___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_3;
x_3 = 1;
return x_3;
}
else
{
uint8_t x_4;
x_4 = 0;
return x_4;
}
}
else
{
if (lean_obj_tag(x_2) == 0)
{
uint8_t x_5;
x_5 = 0;
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; size_t x_10; size_t x_11; uint8_t x_12;
x_6 = lean_ctor_get(x_1, 0);
x_7 = lean_ctor_get(x_1, 1);
x_8 = lean_ctor_get(x_2, 0);
x_9 = lean_ctor_get(x_2, 1);
x_10 = lean_ptr_addr(x_6);
x_11 = lean_ptr_addr(x_8);
x_12 = lean_usize_dec_eq(x_10, x_11);
if (x_12 == 0)
{
uint8_t x_13;
x_13 = 0;
return x_13;
}
else
{
x_1 = x_7;
x_2 = x_9;
goto _start;
}
}
}
}
}
LEAN_EXPORT lean_object* l_ptrEqList(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_ptrEqList___rarg___boxed), 2, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_ptrEqList___rarg___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_ptrEqList___rarg(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_withPtrEqUnsafe___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -494,7 +600,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_getElem_x21___rarg___closed__1;
x_2 = l_getElem_x21___rarg___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_getElem_x21___rarg___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Compiler/IR/Basic.c generated
View file

@ -12616,7 +12616,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at_Lean_IR_addParamsRename___spec__2___closed__1;
x_2 = l_Std_Range_forIn_loop___at_Lean_IR_addParamsRename___spec__2___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at_Lean_IR_addParamsRename___spec__2___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Compiler/IR/Borrow.c generated
View file

@ -3380,7 +3380,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Nat_forM_loop___at_Lean_IR_Borrow_ownArgsUsingParams___spec__2___closed__1;
x_2 = l_Nat_forM_loop___at_Lean_IR_Borrow_ownArgsUsingParams___spec__2___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Nat_forM_loop___at_Lean_IR_Borrow_ownArgsUsingParams___spec__2___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Compiler/IR/Boxing.c generated
View file

@ -466,7 +466,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Nat_foldM_loop___at_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___spec__2___closed__1;
x_2 = l_Nat_foldM_loop___at_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___spec__2___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Nat_foldM_loop___at_Lean_IR_ExplicitBoxing_mkBoxedVersionAux___spec__2___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Compiler/IR/ElimDeadBranches.c generated
View file

@ -2112,7 +2112,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Nat_foldAux___at_Lean_IR_UnreachableBranches_Value_merge___spec__2___closed__1;
x_2 = l_Nat_foldAux___at_Lean_IR_UnreachableBranches_Value_merge___spec__2___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Nat_foldAux___at_Lean_IR_UnreachableBranches_Value_merge___spec__2___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Compiler/IR/EmitC.c generated
View file

@ -1782,7 +1782,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Nat_forM_loop___at_Lean_IR_EmitC_emitFnDeclAux___spec__1___lambda__1___closed__1;
x_2 = l_Nat_forM_loop___at_Lean_IR_EmitC_emitFnDeclAux___spec__1___lambda__1___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Nat_forM_loop___at_Lean_IR_EmitC_emitFnDeclAux___spec__1___lambda__1___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Compiler/IR/ExpandResetReuse.c generated
View file

@ -989,7 +989,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_IR_ExpandResetReuse_eraseProjIncForAux___closed__1;
x_2 = l_Lean_IR_ExpandResetReuse_eraseProjIncForAux___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Lean_IR_ExpandResetReuse_eraseProjIncForAux___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Compiler/IR/RC.c generated
View file

@ -3513,7 +3513,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Nat_anyAux___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_isFirstOcc___spec__3___closed__1;
x_2 = l_Nat_anyAux___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_isFirstOcc___spec__3___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Nat_anyAux___at___private_Lean_Compiler_IR_RC_0__Lean_IR_ExplicitRC_isFirstOcc___spec__3___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Compiler/IR/SimpCase.c generated
View file

@ -261,7 +261,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_getOccsOf___spec__2___closed__1;
x_2 = l_Std_Range_forIn_loop___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_getOccsOf___spec__2___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at___private_Lean_Compiler_IR_SimpCase_0__Lean_IR_getOccsOf___spec__2___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

8
stage0/stdlib/Lean/Data/Lsp/Capabilities.c generated
View file

@ -41,7 +41,7 @@ LEAN_EXPORT lean_object* l_Lean_Lsp_instFromJsonServerCapabilities;
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonClientCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_399____spec__1___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Lsp_instToJsonCompletionClientCapabilities___closed__1;
static lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_594____closed__2;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3468_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3532_(lean_object*);
LEAN_EXPORT uint8_t l_Lean_Lsp_ServerCapabilities_workspaceSymbolProvider___default;
LEAN_EXPORT lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonClientCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_425____spec__1___boxed(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_Lsp_ServerCapabilities_hoverProvider___default;
@ -59,7 +59,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_from
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonClientCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_399____spec__2(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonCompletionOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_115_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_723____spec__1___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3396_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3460_(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Lsp_ClientCapabilities_textDocument_x3f___default;
LEAN_EXPORT lean_object* l_Lean_Lsp_instFromJsonTextDocumentClientCapabilities;
static lean_object* l_Lean_Lsp_instToJsonShowDocumentClientCapabilities___closed__1;
@ -1777,7 +1777,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_obj
x_4 = lean_ctor_get(x_2, 0);
lean_inc(x_4);
lean_dec(x_2);
x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3468_(x_4);
x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3532_(x_4);
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_5);
@ -2192,7 +2192,7 @@ return x_4;
else
{
lean_object* x_5;
x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3396_(x_3);
x_5 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonSemanticTokensOptions____x40_Lean_Data_Lsp_LanguageFeatures___hyg_3460_(x_3);
lean_dec(x_3);
if (lean_obj_tag(x_5) == 0)
{

1368
stage0/stdlib/Lean/Data/Lsp/LanguageFeatures.c generated
View file

File diff suppressed because it is too large Load diff

2
stage0/stdlib/Lean/Data/Position.c generated
View file

@ -922,7 +922,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_FileMap_toPosition_loop___closed__1;
x_2 = l_Lean_FileMap_toPosition_loop___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Lean_FileMap_toPosition_loop___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/App.c generated
View file

@ -14042,7 +14042,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_anyNamedArgDependsOnCurrent___spec__51___closed__3;
x_2 = l_Std_Range_forIn_loop___at___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_anyNamedArgDependsOnCurrent___spec__51___closed__4;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at___private_Lean_Elab_App_0__Lean_Elab_Term_ElabAppArgs_anyNamedArgDependsOnCurrent___spec__51___closed__5;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/Binders.c generated
View file

@ -7236,7 +7236,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Elab_Term_elabBinder___rarg___lambda__1___closed__1;
x_2 = l_Lean_Elab_Term_elabBinder___rarg___lambda__1___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Lean_Elab_Term_elabBinder___rarg___lambda__1___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@ -6866,7 +6866,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_resolveNameUsingNamespacesCore___at_Lean_Elab_Command_elabExport___spec__3___lambda__1___closed__3;
x_2 = l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_resolveNameUsingNamespacesCore___at_Lean_Elab_Command_elabExport___spec__3___lambda__1___closed__4;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_resolveNameUsingNamespacesCore___at_Lean_Elab_Command_elabExport___spec__3___lambda__1___closed__5;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/BuiltinNotation.c generated
View file

@ -1545,7 +1545,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at_Lean_Elab_Term_elabAnonymousCtor___spec__3___closed__1;
x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Term_elabAnonymousCtor___spec__3___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at_Lean_Elab_Term_elabAnonymousCtor___spec__3___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@ -13346,7 +13346,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_resolveNameUsingNamespacesCore___at_Lean_Elab_Term_elabOpen___spec__22___lambda__1___closed__3;
x_2 = l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_resolveNameUsingNamespacesCore___at_Lean_Elab_Term_elabOpen___spec__22___lambda__1___closed__4;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_resolveNameUsingNamespacesCore___at_Lean_Elab_Term_elabOpen___spec__22___lambda__1___closed__5;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/ComputedFields.c generated
View file

@ -6512,7 +6512,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Elab_ComputedFields_overrideCasesOn___lambda__3___closed__3;
x_2 = l_Lean_Elab_ComputedFields_overrideCasesOn___lambda__3___closed__4;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Lean_Elab_ComputedFields_overrideCasesOn___lambda__3___closed__5;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

6233
stage0/stdlib/Lean/Elab/Declaration.c generated
View file

File diff suppressed because it is too large Load diff

2
stage0/stdlib/Lean/Elab/Deriving/BEq.c generated
View file

@ -1306,7 +1306,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_BEq_mkMatch_mkAlts___spec__4___closed__15;
x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_BEq_mkMatch_mkAlts___spec__4___closed__16;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_BEq_mkMatch_mkAlts___spec__4___closed__17;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/Deriving/Basic.c generated
View file

@ -2216,7 +2216,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Array_forInUnsafe_loop___at_Lean_Elab_elabDeriving___spec__19___closed__1;
x_2 = l_Array_forInUnsafe_loop___at_Lean_Elab_elabDeriving___spec__19___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Array_forInUnsafe_loop___at_Lean_Elab_elabDeriving___spec__19___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/Deriving/DecEq.c generated
View file

@ -2978,7 +2978,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_DecEq_mkMatch_mkAlts___spec__5___closed__5;
x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_DecEq_mkMatch_mkAlts___spec__5___closed__6;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_DecEq_mkMatch_mkAlts___spec__5___closed__7;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

1693
stage0/stdlib/Lean/Elab/Deriving/FromToJson.c generated
View file

File diff suppressed because it is too large Load diff

2
stage0/stdlib/Lean/Elab/Deriving/Hashable.c generated
View file

@ -877,7 +877,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__26;
x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__27;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__28;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/Deriving/Inhabited.c generated
View file

@ -10170,7 +10170,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at___private_Lean_Elab_Deriving_Inhabited_0__Lean_Elab_mkInhabitedInstanceUsing_mkInstanceCmd_x3f___spec__1___closed__5;
x_2 = l_Std_Range_forIn_loop___at___private_Lean_Elab_Deriving_Inhabited_0__Lean_Elab_mkInhabitedInstanceUsing_mkInstanceCmd_x3f___spec__1___closed__6;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at___private_Lean_Elab_Deriving_Inhabited_0__Lean_Elab_mkInhabitedInstanceUsing_mkInstanceCmd_x3f___spec__1___closed__7;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/Deriving/Ord.c generated
View file

@ -1499,7 +1499,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Ord_mkMatch_mkAlts___spec__5___closed__5;
x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Ord_mkMatch_mkAlts___spec__5___closed__6;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Ord_mkMatch_mkAlts___spec__5___closed__7;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/Deriving/Repr.c generated
View file

@ -1843,7 +1843,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Repr_mkBodyForStruct___spec__3___closed__5;
x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Repr_mkBodyForStruct___spec__3___closed__6;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Repr_mkBodyForStruct___spec__3___closed__7;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/Deriving/Util.c generated
View file

@ -1109,7 +1109,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_mkInstImplicitBinders___spec__1___closed__5;
x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_mkInstImplicitBinders___spec__1___closed__6;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_mkInstImplicitBinders___spec__1___closed__7;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/Do.c generated
View file

@ -16444,7 +16444,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkTuple___closed__1;
x_2 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkTuple___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_mkTuple___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@ -1136,7 +1136,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_elabElabRulesAux___spec__5___closed__9;
x_2 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_elabElabRulesAux___spec__5___closed__10;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_elabElabRulesAux___spec__5___closed__11;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/Extra.c generated
View file

@ -13851,7 +13851,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__4___closed__9;
x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__4___closed__10;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at_Lean_Elab_Term_BinOp_elabBinCalc___spec__4___closed__11;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

File diff suppressed because it is too large Load diff

2
stage0/stdlib/Lean/Elab/LetRec.c generated
View file

@ -3934,7 +3934,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_elabLetRecDeclValues___spec__1___closed__1;
x_2 = l_Std_Range_forIn_loop___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_elabLetRecDeclValues___spec__1___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_elabLetRecDeclValues___spec__1___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@ -68,12 +68,12 @@ static lean_object* l_Lean_Elab_Level_elabLevel___closed__25;
LEAN_EXPORT lean_object* l_Lean_Elab_Level_mkFreshLevelMVar(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Level_instMonadOptionsLevelElabM___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_Level_maxUniverseOffset;
lean_object* lean_level_mk_max_simp(lean_object*, lean_object*);
lean_object* l_Lean_mkLevelMax_x27(lean_object*, lean_object*);
lean_object* l_Lean_Name_num___override(lean_object*, lean_object*);
lean_object* l_Lean_replaceRef(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at_Lean_Elab_Level_elabLevel___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Elab_Level_mkFreshLevelMVar___spec__2___boxed(lean_object*);
lean_object* lean_level_mk_imax_simp(lean_object*, lean_object*);
lean_object* l_Lean_mkLevelIMax_x27(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Level_initFn____x40_Lean_Elab_Level___hyg_266_(lean_object*);
static lean_object* l_Lean_Elab_Level_elabLevel___closed__12;
lean_object* l_Nat_repr(lean_object*);
@ -1074,7 +1074,7 @@ lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = lean_level_mk_imax_simp(x_12, x_4);
x_14 = l_Lean_mkLevelIMax_x27(x_12, x_4);
x_2 = x_9;
x_4 = x_14;
x_6 = x_13;
@ -1137,7 +1137,7 @@ lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = lean_level_mk_max_simp(x_12, x_4);
x_14 = l_Lean_mkLevelMax_x27(x_12, x_4);
x_2 = x_9;
x_4 = x_14;
x_6 = x_13;

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

@ -925,7 +925,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_elabMacroRulesAux___spec__5___closed__9;
x_2 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_elabMacroRulesAux___spec__5___closed__10;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Array_mapMUnsafe_map___at_Lean_Elab_Command_elabMacroRulesAux___spec__5___closed__11;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

303
stage0/stdlib/Lean/Elab/Match.c generated
View file

@ -98,7 +98,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabPatte
LEAN_EXPORT lean_object* l_Lean_Elab_Term_ToDepElimPattern_savePatternInfo_go___lambda__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_List_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux___spec__9___lambda__1___closed__4;
LEAN_EXPORT lean_object* l_Std_PersistentArray_anyM___at___private_Lean_Elab_Match_0__Lean_Elab_Term_withToClear___spec__5___boxed(lean_object*, lean_object*);
lean_object* lean_expr_update_mdata(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_elabMatch_elabMatchDefault___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_append___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withIncRecDepth___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrs___spec__13___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -635,7 +634,6 @@ static lean_object* l_List_forIn_loop___at_Lean_Elab_Term_reportMatcherResultErr
LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitApp___at___private_Lean_Elab_Match_0__Lean_Elab_Term_withToClear___spec__12(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_AssocList_contains___at___private_Lean_Elab_Match_0__Lean_Elab_Term_ToDepElimPattern_mkPatternRefMap_go___spec__3___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_Term_elabMatch_elabMatchDefault___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_update_proj(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabPatterns___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_Match_0__Lean_Elab_Term_expandNonAtomicDiscrs_x3f___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_eraseIndices(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -685,6 +683,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortTerm___at_Lean_Elab_Term_isAtomic
uint8_t l_Array_contains___at___private_Lean_Meta_Match_Value_0__Lean_Meta_isUIntTypeName___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrs___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_withPatternElabConfig___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_ptr_addr(lean_object*);
LEAN_EXPORT lean_object* l_Array_filterMapM___at___private_Lean_Elab_Match_0__Lean_Elab_Term_getMatchAlts___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Elab_Term_reportMatcherResultErrors___spec__1(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_withLocalDecl___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrs___spec__7___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -947,6 +946,7 @@ static lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchAux__
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_ToDepElimPattern_main_unpack_go___spec__1(size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_ToDepElimPattern_withMVar___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkFreshTypeMVar(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_proj___override(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_precheckMatch___spec__5(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Match_0__Lean_Elab_Term_expandSimpleMatch___closed__11;
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrsWitMatchType___spec__1___closed__11;
@ -4293,9 +4293,11 @@ return x_30;
}
case 10:
{
lean_object* x_31; lean_object* x_32;
x_31 = lean_ctor_get(x_17, 1);
lean_object* x_31; lean_object* x_32; lean_object* x_33;
x_31 = lean_ctor_get(x_17, 0);
lean_inc(x_31);
x_32 = lean_ctor_get(x_17, 1);
lean_inc(x_32);
lean_inc(x_13);
lean_inc(x_12);
lean_inc(x_11);
@ -4303,26 +4305,46 @@ lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_32);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_2);
lean_inc(x_1);
x_32 = l_Lean_Meta_transform_visit___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrs___spec__2(x_1, x_2, x_3, x_4, x_5, x_31, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14);
if (lean_obj_tag(x_32) == 0)
x_33 = l_Lean_Meta_transform_visit___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrs___spec__2(x_1, x_2, x_3, x_4, x_5, x_32, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14);
if (lean_obj_tag(x_33) == 0)
{
lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
x_33 = lean_ctor_get(x_32, 0);
lean_inc(x_33);
x_34 = lean_ctor_get(x_32, 1);
lean_object* x_34; lean_object* x_35; size_t x_36; size_t x_37; uint8_t x_38;
x_34 = lean_ctor_get(x_33, 0);
lean_inc(x_34);
x_35 = lean_ctor_get(x_33, 1);
lean_inc(x_35);
lean_dec(x_33);
x_36 = lean_ptr_addr(x_32);
lean_dec(x_32);
x_35 = lean_expr_update_mdata(x_17, x_33);
x_36 = l_Lean_Meta_transform_visit_visitPost___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrs___spec__3(x_1, x_2, x_3, x_4, x_5, x_35, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_34);
return x_36;
x_37 = lean_ptr_addr(x_34);
x_38 = lean_usize_dec_eq(x_36, x_37);
if (x_38 == 0)
{
lean_object* x_39; lean_object* x_40;
lean_dec(x_17);
x_39 = l_Lean_Expr_mdata___override(x_31, x_34);
x_40 = l_Lean_Meta_transform_visit_visitPost___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrs___spec__3(x_1, x_2, x_3, x_4, x_5, x_39, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_35);
return x_40;
}
else
{
uint8_t x_37;
lean_object* x_41;
lean_dec(x_34);
lean_dec(x_31);
x_41 = l_Lean_Meta_transform_visit_visitPost___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrs___spec__3(x_1, x_2, x_3, x_4, x_5, x_17, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_35);
return x_41;
}
}
else
{
uint8_t x_42;
lean_dec(x_32);
lean_dec(x_31);
lean_dec(x_17);
lean_dec(x_13);
lean_dec(x_12);
@ -4335,31 +4357,35 @@ lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_37 = !lean_is_exclusive(x_32);
if (x_37 == 0)
x_42 = !lean_is_exclusive(x_33);
if (x_42 == 0)
{
return x_32;
return x_33;
}
else
{
lean_object* x_38; lean_object* x_39; lean_object* x_40;
x_38 = lean_ctor_get(x_32, 0);
x_39 = lean_ctor_get(x_32, 1);
lean_inc(x_39);
lean_inc(x_38);
lean_dec(x_32);
x_40 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_40, 0, x_38);
lean_ctor_set(x_40, 1, x_39);
return x_40;
lean_object* x_43; lean_object* x_44; lean_object* x_45;
x_43 = lean_ctor_get(x_33, 0);
x_44 = lean_ctor_get(x_33, 1);
lean_inc(x_44);
lean_inc(x_43);
lean_dec(x_33);
x_45 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_45, 0, x_43);
lean_ctor_set(x_45, 1, x_44);
return x_45;
}
}
}
case 11:
{
lean_object* x_41; lean_object* x_42;
x_41 = lean_ctor_get(x_17, 2);
lean_inc(x_41);
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49;
x_46 = lean_ctor_get(x_17, 0);
lean_inc(x_46);
x_47 = lean_ctor_get(x_17, 1);
lean_inc(x_47);
x_48 = lean_ctor_get(x_17, 2);
lean_inc(x_48);
lean_inc(x_13);
lean_inc(x_12);
lean_inc(x_11);
@ -4367,26 +4393,48 @@ lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_48);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_2);
lean_inc(x_1);
x_42 = l_Lean_Meta_transform_visit___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrs___spec__2(x_1, x_2, x_3, x_4, x_5, x_41, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14);
if (lean_obj_tag(x_42) == 0)
x_49 = l_Lean_Meta_transform_visit___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrs___spec__2(x_1, x_2, x_3, x_4, x_5, x_48, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14);
if (lean_obj_tag(x_49) == 0)
{
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46;
x_43 = lean_ctor_get(x_42, 0);
lean_inc(x_43);
x_44 = lean_ctor_get(x_42, 1);
lean_inc(x_44);
lean_dec(x_42);
x_45 = lean_expr_update_proj(x_17, x_43);
x_46 = l_Lean_Meta_transform_visit_visitPost___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrs___spec__3(x_1, x_2, x_3, x_4, x_5, x_45, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_44);
return x_46;
lean_object* x_50; lean_object* x_51; size_t x_52; size_t x_53; uint8_t x_54;
x_50 = lean_ctor_get(x_49, 0);
lean_inc(x_50);
x_51 = lean_ctor_get(x_49, 1);
lean_inc(x_51);
lean_dec(x_49);
x_52 = lean_ptr_addr(x_48);
lean_dec(x_48);
x_53 = lean_ptr_addr(x_50);
x_54 = lean_usize_dec_eq(x_52, x_53);
if (x_54 == 0)
{
lean_object* x_55; lean_object* x_56;
lean_dec(x_17);
x_55 = l_Lean_Expr_proj___override(x_46, x_47, x_50);
x_56 = l_Lean_Meta_transform_visit_visitPost___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrs___spec__3(x_1, x_2, x_3, x_4, x_5, x_55, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_51);
return x_56;
}
else
{
uint8_t x_47;
lean_object* x_57;
lean_dec(x_50);
lean_dec(x_47);
lean_dec(x_46);
x_57 = l_Lean_Meta_transform_visit_visitPost___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrs___spec__3(x_1, x_2, x_3, x_4, x_5, x_17, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_51);
return x_57;
}
}
else
{
uint8_t x_58;
lean_dec(x_48);
lean_dec(x_47);
lean_dec(x_46);
lean_dec(x_17);
lean_dec(x_13);
lean_dec(x_12);
@ -4399,31 +4447,31 @@ lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_47 = !lean_is_exclusive(x_42);
if (x_47 == 0)
x_58 = !lean_is_exclusive(x_49);
if (x_58 == 0)
{
return x_42;
return x_49;
}
else
{
lean_object* x_48; lean_object* x_49; lean_object* x_50;
x_48 = lean_ctor_get(x_42, 0);
x_49 = lean_ctor_get(x_42, 1);
lean_inc(x_49);
lean_inc(x_48);
lean_dec(x_42);
x_50 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_50, 0, x_48);
lean_ctor_set(x_50, 1, x_49);
return x_50;
lean_object* x_59; lean_object* x_60; lean_object* x_61;
x_59 = lean_ctor_get(x_49, 0);
x_60 = lean_ctor_get(x_49, 1);
lean_inc(x_60);
lean_inc(x_59);
lean_dec(x_49);
x_61 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_61, 0, x_59);
lean_ctor_set(x_61, 1, x_60);
return x_61;
}
}
}
default:
{
lean_object* x_51;
x_51 = l_Lean_Meta_transform_visit_visitPost___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrs___spec__3(x_1, x_2, x_3, x_4, x_5, x_17, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14);
return x_51;
lean_object* x_62;
x_62 = l_Lean_Meta_transform_visit_visitPost___at___private_Lean_Elab_Match_0__Lean_Elab_Term_elabMatchTypeAndDiscrs_elabDiscrs___spec__3(x_1, x_2, x_3, x_4, x_5, x_17, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14);
return x_62;
}
}
}
@ -8912,7 +8960,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_findDiscrRefinementPath_goIndex___spec__1___closed__1;
x_2 = l_Std_Range_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_findDiscrRefinementPath_goIndex___spec__1___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at___private_Lean_Elab_Match_0__Lean_Elab_Term_findDiscrRefinementPath_goIndex___spec__1___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -25136,74 +25184,119 @@ return x_111;
}
case 11:
{
lean_object* x_112; lean_object* x_113;
x_112 = lean_ctor_get(x_1, 2);
lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115;
x_112 = lean_ctor_get(x_1, 0);
lean_inc(x_112);
x_113 = l_Lean_Elab_Term_ToDepElimPattern_savePatternInfo_go(x_112, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_113) == 0)
x_113 = lean_ctor_get(x_1, 1);
lean_inc(x_113);
x_114 = lean_ctor_get(x_1, 2);
lean_inc(x_114);
lean_inc(x_114);
x_115 = l_Lean_Elab_Term_ToDepElimPattern_savePatternInfo_go(x_114, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
if (lean_obj_tag(x_115) == 0)
{
uint8_t x_114;
x_114 = !lean_is_exclusive(x_113);
if (x_114 == 0)
uint8_t x_116;
x_116 = !lean_is_exclusive(x_115);
if (x_116 == 0)
{
lean_object* x_115; lean_object* x_116;
x_115 = lean_ctor_get(x_113, 0);
x_116 = lean_expr_update_proj(x_1, x_115);
lean_ctor_set(x_113, 0, x_116);
return x_113;
}
else
lean_object* x_117; size_t x_118; size_t x_119; uint8_t x_120;
x_117 = lean_ctor_get(x_115, 0);
x_118 = lean_ptr_addr(x_114);
lean_dec(x_114);
x_119 = lean_ptr_addr(x_117);
x_120 = lean_usize_dec_eq(x_118, x_119);
if (x_120 == 0)
{
lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120;
x_117 = lean_ctor_get(x_113, 0);
x_118 = lean_ctor_get(x_113, 1);
lean_inc(x_118);
lean_inc(x_117);
lean_dec(x_113);
x_119 = lean_expr_update_proj(x_1, x_117);
x_120 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_120, 0, x_119);
lean_ctor_set(x_120, 1, x_118);
return x_120;
}
}
else
{
uint8_t x_121;
lean_object* x_121;
lean_dec(x_1);
x_121 = !lean_is_exclusive(x_113);
if (x_121 == 0)
{
return x_113;
x_121 = l_Lean_Expr_proj___override(x_112, x_113, x_117);
lean_ctor_set(x_115, 0, x_121);
return x_115;
}
else
{
lean_object* x_122; lean_object* x_123; lean_object* x_124;
x_122 = lean_ctor_get(x_113, 0);
x_123 = lean_ctor_get(x_113, 1);
lean_dec(x_117);
lean_dec(x_113);
lean_dec(x_112);
lean_ctor_set(x_115, 0, x_1);
return x_115;
}
}
else
{
lean_object* x_122; lean_object* x_123; size_t x_124; size_t x_125; uint8_t x_126;
x_122 = lean_ctor_get(x_115, 0);
x_123 = lean_ctor_get(x_115, 1);
lean_inc(x_123);
lean_inc(x_122);
lean_dec(x_115);
x_124 = lean_ptr_addr(x_114);
lean_dec(x_114);
x_125 = lean_ptr_addr(x_122);
x_126 = lean_usize_dec_eq(x_124, x_125);
if (x_126 == 0)
{
lean_object* x_127; lean_object* x_128;
lean_dec(x_1);
x_127 = l_Lean_Expr_proj___override(x_112, x_113, x_122);
x_128 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_128, 0, x_127);
lean_ctor_set(x_128, 1, x_123);
return x_128;
}
else
{
lean_object* x_129;
lean_dec(x_122);
lean_dec(x_113);
x_124 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_124, 0, x_122);
lean_ctor_set(x_124, 1, x_123);
return x_124;
lean_dec(x_112);
x_129 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_129, 0, x_1);
lean_ctor_set(x_129, 1, x_123);
return x_129;
}
}
}
else
{
uint8_t x_130;
lean_dec(x_114);
lean_dec(x_113);
lean_dec(x_112);
lean_dec(x_1);
x_130 = !lean_is_exclusive(x_115);
if (x_130 == 0)
{
return x_115;
}
else
{
lean_object* x_131; lean_object* x_132; lean_object* x_133;
x_131 = lean_ctor_get(x_115, 0);
x_132 = lean_ctor_get(x_115, 1);
lean_inc(x_132);
lean_inc(x_131);
lean_dec(x_115);
x_133 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_133, 0, x_131);
lean_ctor_set(x_133, 1, x_132);
return x_133;
}
}
}
default:
{
lean_object* x_125;
lean_object* x_134;
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_125 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_125, 0, x_1);
lean_ctor_set(x_125, 1, x_9);
return x_125;
x_134 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_134, 0, x_1);
lean_ctor_set(x_134, 1, x_9);
return x_134;
}
}
}

2
stage0/stdlib/Lean/Elab/MutualDef.c generated
View file

@ -2636,7 +2636,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_isMultiConstant_x3f___closed__1;
x_2 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_isMultiConstant_x3f___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_isMultiConstant_x3f___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@ -1945,7 +1945,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Syntax_instForInTopDownSyntax_loop___at_Lean_Elab_Command_hasDuplicateAntiquot___spec__1___closed__4;
x_2 = l_Lean_Syntax_instForInTopDownSyntax_loop___at_Lean_Elab_Command_hasDuplicateAntiquot___spec__1___closed__5;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Lean_Syntax_instForInTopDownSyntax_loop___at_Lean_Elab_Command_hasDuplicateAntiquot___spec__1___closed__6;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@ -3641,7 +3641,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_resolveNameUsingNamespacesCore___rarg___lambda__2___closed__3;
x_2 = l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_resolveNameUsingNamespacesCore___rarg___lambda__2___closed__4;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_resolveNameUsingNamespacesCore___rarg___lambda__2___closed__5;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/PatternVar.c generated
View file

@ -1169,7 +1169,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_getNextParam___closed__1;
x_2 = l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_getNextParam___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_getNextParam___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/PreDefinition/Basic.c generated
View file

@ -5186,7 +5186,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Elab_addAndCompileUnsafe___closed__1;
x_2 = l_Lean_Elab_addAndCompileUnsafe___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Lean_Elab_addAndCompileUnsafe___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@ -338,7 +338,6 @@ LEAN_EXPORT lean_object* l_Array_foldrMUnsafe_fold___at___private_Lean_Elab_PreD
lean_object* l_Lean_Meta_delta_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_replaceFVarId(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Eqns_deltaRHS_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_update_proj(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentArray_forIn___at___private_Lean_Elab_PreDefinition_Eqns_0__Lean_Elab_Eqns_saveEqn___spec__27___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_commitWhenSome_x3f___at_Lean_Elab_Eqns_funext_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Elab_Eqns_mkEqnTypes_go___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -376,6 +375,7 @@ LEAN_EXPORT lean_object* l_Lean_ForEachExpr_visit___at_Lean_Elab_Eqns_simpEqnTyp
LEAN_EXPORT lean_object* l_Lean_Elab_Eqns_simpEqnType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_fvar___override(lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Eqns_removeUnusedEqnHypotheses_go___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_ptr_addr(lean_object*);
static lean_object* l_Lean_Elab_Eqns_deltaLHS___lambda__2___closed__9;
lean_object* l_Std_PersistentArray_push___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Expr_const___override(lean_object*, lean_object*);
@ -491,6 +491,7 @@ LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Elab_Eqns_removeUnusedEqnHyp
static lean_object* l_Lean_Elab_Eqns_splitMatch_x3f_go___closed__5;
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Eqns_removeUnusedEqnHypotheses_go___spec__11(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Eqns_mkUnfoldProof___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_proj___override(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAtAux___at_Lean_Elab_Eqns_getUnfoldFor_x3f___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Eqns_removeUnusedEqnHypotheses_go___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Eqns_0__Lean_Elab_Eqns_saveEqn___spec__31(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1746,7 +1747,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_Eqns_0__Lean_Elab_Eqns_findMatchToSplit_x3f___spec__1___closed__1;
x_2 = l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_Eqns_0__Lean_Elab_Eqns_findMatchToSplit_x3f___spec__1___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_Eqns_0__Lean_Elab_Eqns_findMatchToSplit_x3f___spec__1___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -20116,80 +20117,128 @@ x_10 = lean_ctor_get(x_7, 1);
x_11 = l_Lean_Expr_getAppFn(x_9);
if (lean_obj_tag(x_11) == 11)
{
lean_object* x_12; lean_object* x_13;
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
lean_free_object(x_7);
x_12 = lean_ctor_get(x_11, 2);
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
x_13 = l___private_Lean_Elab_PreDefinition_Eqns_0__Lean_Elab_Eqns_whnfAux(x_12, x_2, x_3, x_4, x_5, x_10);
if (lean_obj_tag(x_13) == 0)
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
x_14 = lean_ctor_get(x_11, 2);
lean_inc(x_14);
lean_inc(x_14);
x_15 = l___private_Lean_Elab_PreDefinition_Eqns_0__Lean_Elab_Eqns_whnfAux(x_14, x_2, x_3, x_4, x_5, x_10);
if (lean_obj_tag(x_15) == 0)
{
uint8_t x_14;
x_14 = !lean_is_exclusive(x_13);
if (x_14 == 0)
uint8_t x_16;
x_16 = !lean_is_exclusive(x_15);
if (x_16 == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_15 = lean_ctor_get(x_13, 0);
x_16 = lean_expr_update_proj(x_11, x_15);
x_17 = lean_unsigned_to_nat(0u);
x_18 = l___private_Lean_Expr_0__Lean_Expr_getAppNumArgsAux(x_9, x_17);
x_19 = l___private_Lean_Elab_PreDefinition_Eqns_0__Lean_Elab_Eqns_findMatchToSplit_x3f___lambda__3___closed__5;
lean_inc(x_18);
x_20 = lean_mk_array(x_18, x_19);
x_21 = lean_unsigned_to_nat(1u);
x_22 = lean_nat_sub(x_18, x_21);
lean_dec(x_18);
x_23 = l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(x_9, x_20, x_22);
x_24 = l_Lean_mkAppN(x_16, x_23);
lean_ctor_set(x_13, 0, x_24);
return x_13;
lean_object* x_17; size_t x_18; size_t x_19; uint8_t x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_17 = lean_ctor_get(x_15, 0);
x_18 = lean_ptr_addr(x_14);
lean_dec(x_14);
x_19 = lean_ptr_addr(x_17);
x_20 = lean_usize_dec_eq(x_18, x_19);
x_21 = lean_unsigned_to_nat(0u);
x_22 = l___private_Lean_Expr_0__Lean_Expr_getAppNumArgsAux(x_9, x_21);
x_23 = l___private_Lean_Elab_PreDefinition_Eqns_0__Lean_Elab_Eqns_findMatchToSplit_x3f___lambda__3___closed__5;
lean_inc(x_22);
x_24 = lean_mk_array(x_22, x_23);
x_25 = lean_unsigned_to_nat(1u);
x_26 = lean_nat_sub(x_22, x_25);
lean_dec(x_22);
x_27 = l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(x_9, x_24, x_26);
if (x_20 == 0)
{
lean_object* x_28; lean_object* x_29;
lean_dec(x_11);
x_28 = l_Lean_Expr_proj___override(x_12, x_13, x_17);
x_29 = l_Lean_mkAppN(x_28, x_27);
lean_ctor_set(x_15, 0, x_29);
return x_15;
}
else
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
x_25 = lean_ctor_get(x_13, 0);
x_26 = lean_ctor_get(x_13, 1);
lean_inc(x_26);
lean_inc(x_25);
lean_object* x_30;
lean_dec(x_17);
lean_dec(x_13);
x_27 = lean_expr_update_proj(x_11, x_25);
x_28 = lean_unsigned_to_nat(0u);
x_29 = l___private_Lean_Expr_0__Lean_Expr_getAppNumArgsAux(x_9, x_28);
x_30 = l___private_Lean_Elab_PreDefinition_Eqns_0__Lean_Elab_Eqns_findMatchToSplit_x3f___lambda__3___closed__5;
lean_inc(x_29);
x_31 = lean_mk_array(x_29, x_30);
x_32 = lean_unsigned_to_nat(1u);
x_33 = lean_nat_sub(x_29, x_32);
lean_dec(x_29);
x_34 = l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(x_9, x_31, x_33);
x_35 = l_Lean_mkAppN(x_27, x_34);
x_36 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_36, 0, x_35);
lean_ctor_set(x_36, 1, x_26);
return x_36;
lean_dec(x_12);
x_30 = l_Lean_mkAppN(x_11, x_27);
lean_ctor_set(x_15, 0, x_30);
return x_15;
}
}
else
{
uint8_t x_37;
lean_object* x_31; lean_object* x_32; size_t x_33; size_t x_34; uint8_t x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42;
x_31 = lean_ctor_get(x_15, 0);
x_32 = lean_ctor_get(x_15, 1);
lean_inc(x_32);
lean_inc(x_31);
lean_dec(x_15);
x_33 = lean_ptr_addr(x_14);
lean_dec(x_14);
x_34 = lean_ptr_addr(x_31);
x_35 = lean_usize_dec_eq(x_33, x_34);
x_36 = lean_unsigned_to_nat(0u);
x_37 = l___private_Lean_Expr_0__Lean_Expr_getAppNumArgsAux(x_9, x_36);
x_38 = l___private_Lean_Elab_PreDefinition_Eqns_0__Lean_Elab_Eqns_findMatchToSplit_x3f___lambda__3___closed__5;
lean_inc(x_37);
x_39 = lean_mk_array(x_37, x_38);
x_40 = lean_unsigned_to_nat(1u);
x_41 = lean_nat_sub(x_37, x_40);
lean_dec(x_37);
x_42 = l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(x_9, x_39, x_41);
if (x_35 == 0)
{
lean_object* x_43; lean_object* x_44; lean_object* x_45;
lean_dec(x_11);
x_43 = l_Lean_Expr_proj___override(x_12, x_13, x_31);
x_44 = l_Lean_mkAppN(x_43, x_42);
x_45 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_45, 0, x_44);
lean_ctor_set(x_45, 1, x_32);
return x_45;
}
else
{
lean_object* x_46; lean_object* x_47;
lean_dec(x_31);
lean_dec(x_13);
lean_dec(x_12);
x_46 = l_Lean_mkAppN(x_11, x_42);
x_47 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_47, 0, x_46);
lean_ctor_set(x_47, 1, x_32);
return x_47;
}
}
}
else
{
uint8_t x_48;
lean_dec(x_14);
lean_dec(x_13);
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_9);
x_37 = !lean_is_exclusive(x_13);
if (x_37 == 0)
x_48 = !lean_is_exclusive(x_15);
if (x_48 == 0)
{
return x_13;
return x_15;
}
else
{
lean_object* x_38; lean_object* x_39; lean_object* x_40;
x_38 = lean_ctor_get(x_13, 0);
x_39 = lean_ctor_get(x_13, 1);
lean_inc(x_39);
lean_inc(x_38);
lean_dec(x_13);
x_40 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_40, 0, x_38);
lean_ctor_set(x_40, 1, x_39);
return x_40;
lean_object* x_49; lean_object* x_50; lean_object* x_51;
x_49 = lean_ctor_get(x_15, 0);
x_50 = lean_ctor_get(x_15, 1);
lean_inc(x_50);
lean_inc(x_49);
lean_dec(x_15);
x_51 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_51, 0, x_49);
lean_ctor_set(x_51, 1, x_50);
return x_51;
}
}
}
@ -20205,120 +20254,153 @@ return x_7;
}
else
{
lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_41 = lean_ctor_get(x_7, 0);
x_42 = lean_ctor_get(x_7, 1);
lean_inc(x_42);
lean_inc(x_41);
lean_object* x_52; lean_object* x_53; lean_object* x_54;
x_52 = lean_ctor_get(x_7, 0);
x_53 = lean_ctor_get(x_7, 1);
lean_inc(x_53);
lean_inc(x_52);
lean_dec(x_7);
x_43 = l_Lean_Expr_getAppFn(x_41);
if (lean_obj_tag(x_43) == 11)
x_54 = l_Lean_Expr_getAppFn(x_52);
if (lean_obj_tag(x_54) == 11)
{
lean_object* x_44; lean_object* x_45;
x_44 = lean_ctor_get(x_43, 2);
lean_inc(x_44);
x_45 = l___private_Lean_Elab_PreDefinition_Eqns_0__Lean_Elab_Eqns_whnfAux(x_44, x_2, x_3, x_4, x_5, x_42);
if (lean_obj_tag(x_45) == 0)
lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58;
x_55 = lean_ctor_get(x_54, 0);
lean_inc(x_55);
x_56 = lean_ctor_get(x_54, 1);
lean_inc(x_56);
x_57 = lean_ctor_get(x_54, 2);
lean_inc(x_57);
lean_inc(x_57);
x_58 = l___private_Lean_Elab_PreDefinition_Eqns_0__Lean_Elab_Eqns_whnfAux(x_57, x_2, x_3, x_4, x_5, x_53);
if (lean_obj_tag(x_58) == 0)
{
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58;
x_46 = lean_ctor_get(x_45, 0);
lean_inc(x_46);
x_47 = lean_ctor_get(x_45, 1);
lean_inc(x_47);
if (lean_is_exclusive(x_45)) {
lean_ctor_release(x_45, 0);
lean_ctor_release(x_45, 1);
x_48 = x_45;
} else {
lean_dec_ref(x_45);
x_48 = lean_box(0);
}
x_49 = lean_expr_update_proj(x_43, x_46);
x_50 = lean_unsigned_to_nat(0u);
x_51 = l___private_Lean_Expr_0__Lean_Expr_getAppNumArgsAux(x_41, x_50);
x_52 = l___private_Lean_Elab_PreDefinition_Eqns_0__Lean_Elab_Eqns_findMatchToSplit_x3f___lambda__3___closed__5;
lean_inc(x_51);
x_53 = lean_mk_array(x_51, x_52);
x_54 = lean_unsigned_to_nat(1u);
x_55 = lean_nat_sub(x_51, x_54);
lean_dec(x_51);
x_56 = l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(x_41, x_53, x_55);
x_57 = l_Lean_mkAppN(x_49, x_56);
if (lean_is_scalar(x_48)) {
x_58 = lean_alloc_ctor(0, 2, 0);
} else {
x_58 = x_48;
}
lean_ctor_set(x_58, 0, x_57);
lean_ctor_set(x_58, 1, x_47);
return x_58;
}
else
{
lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62;
lean_dec(x_43);
lean_dec(x_41);
x_59 = lean_ctor_get(x_45, 0);
lean_object* x_59; lean_object* x_60; lean_object* x_61; size_t x_62; size_t x_63; uint8_t x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71;
x_59 = lean_ctor_get(x_58, 0);
lean_inc(x_59);
x_60 = lean_ctor_get(x_45, 1);
x_60 = lean_ctor_get(x_58, 1);
lean_inc(x_60);
if (lean_is_exclusive(x_45)) {
lean_ctor_release(x_45, 0);
lean_ctor_release(x_45, 1);
x_61 = x_45;
if (lean_is_exclusive(x_58)) {
lean_ctor_release(x_58, 0);
lean_ctor_release(x_58, 1);
x_61 = x_58;
} else {
lean_dec_ref(x_45);
lean_dec_ref(x_58);
x_61 = lean_box(0);
}
if (lean_is_scalar(x_61)) {
x_62 = lean_alloc_ctor(1, 2, 0);
} else {
x_62 = x_61;
}
lean_ctor_set(x_62, 0, x_59);
lean_ctor_set(x_62, 1, x_60);
return x_62;
}
}
else
{
lean_object* x_63;
lean_dec(x_43);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_63 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_63, 0, x_41);
lean_ctor_set(x_63, 1, x_42);
return x_63;
}
}
}
else
{
uint8_t x_64;
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_64 = !lean_is_exclusive(x_7);
x_62 = lean_ptr_addr(x_57);
lean_dec(x_57);
x_63 = lean_ptr_addr(x_59);
x_64 = lean_usize_dec_eq(x_62, x_63);
x_65 = lean_unsigned_to_nat(0u);
x_66 = l___private_Lean_Expr_0__Lean_Expr_getAppNumArgsAux(x_52, x_65);
x_67 = l___private_Lean_Elab_PreDefinition_Eqns_0__Lean_Elab_Eqns_findMatchToSplit_x3f___lambda__3___closed__5;
lean_inc(x_66);
x_68 = lean_mk_array(x_66, x_67);
x_69 = lean_unsigned_to_nat(1u);
x_70 = lean_nat_sub(x_66, x_69);
lean_dec(x_66);
x_71 = l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(x_52, x_68, x_70);
if (x_64 == 0)
{
lean_object* x_72; lean_object* x_73; lean_object* x_74;
lean_dec(x_54);
x_72 = l_Lean_Expr_proj___override(x_55, x_56, x_59);
x_73 = l_Lean_mkAppN(x_72, x_71);
if (lean_is_scalar(x_61)) {
x_74 = lean_alloc_ctor(0, 2, 0);
} else {
x_74 = x_61;
}
lean_ctor_set(x_74, 0, x_73);
lean_ctor_set(x_74, 1, x_60);
return x_74;
}
else
{
lean_object* x_75; lean_object* x_76;
lean_dec(x_59);
lean_dec(x_56);
lean_dec(x_55);
x_75 = l_Lean_mkAppN(x_54, x_71);
if (lean_is_scalar(x_61)) {
x_76 = lean_alloc_ctor(0, 2, 0);
} else {
x_76 = x_61;
}
lean_ctor_set(x_76, 0, x_75);
lean_ctor_set(x_76, 1, x_60);
return x_76;
}
}
else
{
lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80;
lean_dec(x_57);
lean_dec(x_56);
lean_dec(x_55);
lean_dec(x_54);
lean_dec(x_52);
x_77 = lean_ctor_get(x_58, 0);
lean_inc(x_77);
x_78 = lean_ctor_get(x_58, 1);
lean_inc(x_78);
if (lean_is_exclusive(x_58)) {
lean_ctor_release(x_58, 0);
lean_ctor_release(x_58, 1);
x_79 = x_58;
} else {
lean_dec_ref(x_58);
x_79 = lean_box(0);
}
if (lean_is_scalar(x_79)) {
x_80 = lean_alloc_ctor(1, 2, 0);
} else {
x_80 = x_79;
}
lean_ctor_set(x_80, 0, x_77);
lean_ctor_set(x_80, 1, x_78);
return x_80;
}
}
else
{
lean_object* x_81;
lean_dec(x_54);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_81 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_81, 0, x_52);
lean_ctor_set(x_81, 1, x_53);
return x_81;
}
}
}
else
{
uint8_t x_82;
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
x_82 = !lean_is_exclusive(x_7);
if (x_82 == 0)
{
return x_7;
}
else
{
lean_object* x_65; lean_object* x_66; lean_object* x_67;
x_65 = lean_ctor_get(x_7, 0);
x_66 = lean_ctor_get(x_7, 1);
lean_inc(x_66);
lean_inc(x_65);
lean_object* x_83; lean_object* x_84; lean_object* x_85;
x_83 = lean_ctor_get(x_7, 0);
x_84 = lean_ctor_get(x_7, 1);
lean_inc(x_84);
lean_inc(x_83);
lean_dec(x_7);
x_67 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_67, 0, x_65);
lean_ctor_set(x_67, 1, x_66);
return x_67;
x_85 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_85, 0, x_83);
lean_ctor_set(x_85, 1, x_84);
return x_85;
}
}
}

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

@ -7509,7 +7509,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__22___lambda__3___closed__1;
x_2 = l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__22___lambda__3___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Array_forInUnsafe_loop___at_Lean_Elab_addPreDefinitions___spec__22___lambda__3___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/PreDefinition/MkInhabitant.c generated
View file

@ -570,7 +570,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_PreDefinition_MkInhabitant_0__Lean_Elab_mkFnInhabitant_x3f_loop___closed__2;
x_2 = l___private_Lean_Elab_PreDefinition_MkInhabitant_0__Lean_Elab_mkFnInhabitant_x3f_loop___closed__3;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l___private_Lean_Elab_PreDefinition_MkInhabitant_0__Lean_Elab_mkFnInhabitant_x3f_loop___closed__4;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/PreDefinition/Structural/BRecOn.c generated
View file

@ -1681,7 +1681,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Expr_withAppAux___at___private_Lean_Elab_PreDefinition_Structural_BRecOn_0__Lean_Elab_Structural_withBelowDict___spec__1___rarg___lambda__2___closed__1;
x_2 = l_Lean_Expr_withAppAux___at___private_Lean_Elab_PreDefinition_Structural_BRecOn_0__Lean_Elab_Structural_withBelowDict___spec__1___rarg___lambda__2___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Lean_Expr_withAppAux___at___private_Lean_Elab_PreDefinition_Structural_BRecOn_0__Lean_Elab_Structural_withBelowDict___spec__1___rarg___lambda__2___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@ -1842,7 +1842,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at_Lean_Elab_Structural_mkEqns___spec__1___closed__1;
x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Structural_mkEqns___spec__1___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at_Lean_Elab_Structural_mkEqns___spec__1___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/PreDefinition/Structural/IndPred.c generated
View file

@ -261,7 +261,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_matchMatcherApp_x3f___at___private_Lean_Elab_PreDefinition_Structural_IndPred_0__Lean_Elab_Structural_replaceIndPredRecApps_loop_addBelow___spec__1___closed__2;
x_2 = l_Lean_Meta_matchMatcherApp_x3f___at___private_Lean_Elab_PreDefinition_Structural_IndPred_0__Lean_Elab_Structural_replaceIndPredRecApps_loop_addBelow___spec__1___closed__3;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Lean_Meta_matchMatcherApp_x3f___at___private_Lean_Elab_PreDefinition_Structural_IndPred_0__Lean_Elab_Structural_replaceIndPredRecApps_loop_addBelow___spec__1___closed__4;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/PreDefinition/Structural/Main.c generated
View file

@ -2816,7 +2816,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Elab_Structural_structuralRecursion___closed__6;
x_2 = l_Lean_Elab_Structural_structuralRecursion___closed__7;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Lean_Elab_Structural_structuralRecursion___closed__8;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/PreDefinition/Structural/SmartUnfolding.c generated
View file

@ -141,7 +141,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_matchMatcherApp_x3f___at_Lean_Elab_Structural_addSmartUnfoldingDefAux_visit___spec__1___closed__2;
x_2 = l_Lean_Meta_matchMatcherApp_x3f___at_Lean_Elab_Structural_addSmartUnfoldingDefAux_visit___spec__1___closed__3;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Lean_Meta_matchMatcherApp_x3f___at_Lean_Elab_Structural_addSmartUnfoldingDefAux_visit___spec__1___closed__4;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@ -2207,7 +2207,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_decodePackedArg_x3f___closed__1;
x_2 = l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_decodePackedArg_x3f___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l___private_Lean_Elab_PreDefinition_WF_Eqns_0__Lean_Elab_WF_decodePackedArg_x3f___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

6
stage0/stdlib/Lean/Elab/PreDefinition/WF/Fix.c generated
View file

@ -59,7 +59,6 @@ lean_object* l_Array_extract___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_CasesOnApp_addArg_x3f(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getRecAppSyntax_x3f(lean_object*);
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*);
lean_object* l_Lean_Elab_Tactic_evalTacticAux(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_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_replaceRecApps___lambda__2___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_getMatcherInfo_x3f___at___private_Lean_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_replaceRecApps_loop___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_replaceRecApps_processRec(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*);
@ -69,6 +68,7 @@ lean_object* lean_st_ref_get(lean_object*, lean_object*);
uint8_t l_Lean_Elab_Structural_recArgHasLooseBVarsAt(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_replaceRecApps___lambda__2___closed__2;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_replaceRecApps_loop___spec__9___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* l_Lean_Elab_Tactic_evalTactic(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_Elab_WF_mkFix___lambda__1___closed__6;
LEAN_EXPORT lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_replaceRecApps_loop___spec__11___rarg(lean_object*, uint8_t, 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_isAppOf(lean_object*, lean_object*);
@ -498,7 +498,7 @@ x_21 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
lean_ctor_set(x_21, 2, x_18);
x_22 = l_Lean_Elab_Tactic_evalTacticAux(x_21, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_14);
x_22 = l_Lean_Elab_Tactic_evalTactic(x_21, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_14);
return x_22;
}
}
@ -985,7 +985,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_replaceRecApps_processRec___closed__2;
x_2 = l___private_Lean_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_replaceRecApps_processRec___closed__3;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l___private_Lean_Elab_PreDefinition_WF_Fix_0__Lean_Elab_WF_replaceRecApps_processRec___closed__4;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/PreDefinition/WF/Ite.c generated
View file

@ -146,7 +146,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Meta_iteToDIte___lambda__1___closed__8;
x_2 = l_Lean_Meta_iteToDIte___lambda__1___closed__9;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Lean_Meta_iteToDIte___lambda__1___closed__10;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@ -257,7 +257,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_isOnlyOneUnaryDef___closed__1;
x_2 = l___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_isOnlyOneUnaryDef___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l___private_Lean_Elab_PreDefinition_WF_Main_0__Lean_Elab_isOnlyOneUnaryDef___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/PreDefinition/WF/PackDomain.c generated
View file

@ -389,7 +389,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Elab_WF_mkUnaryArg_go___closed__1;
x_2 = l_Lean_Elab_WF_mkUnaryArg_go___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Lean_Elab_WF_mkUnaryArg_go___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/PreDefinition/WF/PackMutual.c generated
View file

@ -947,7 +947,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_WF_PackMutual_0__Lean_Elab_WF_getCodomainsLevel___spec__1___closed__2;
x_2 = l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_WF_PackMutual_0__Lean_Elab_WF_getCodomainsLevel___spec__1___closed__3;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at___private_Lean_Elab_PreDefinition_WF_PackMutual_0__Lean_Elab_WF_getCodomainsLevel___spec__1___closed__4;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

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

@ -352,7 +352,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_PreDefinition_WF_Rel_0__Lean_Elab_WF_getRefFromElems___lambda__1___closed__1;
x_2 = l___private_Lean_Elab_PreDefinition_WF_Rel_0__Lean_Elab_WF_getRefFromElems___lambda__1___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l___private_Lean_Elab_PreDefinition_WF_Rel_0__Lean_Elab_WF_getRefFromElems___lambda__1___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/PreDefinition/WF/TerminationHint.c generated
View file

@ -4057,7 +4057,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_WF_TerminationHint_0__Lean_Elab_WF_expandTerminationByNonCore___spec__9___closed__3;
x_2 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_WF_TerminationHint_0__Lean_Elab_WF_expandTerminationByNonCore___spec__9___closed__4;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_WF_TerminationHint_0__Lean_Elab_WF_expandTerminationByNonCore___spec__9___closed__5;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/Quotation.c generated
View file

@ -2931,7 +2931,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Elab_Term_Quotation_mkTuple___closed__10;
x_2 = l_Lean_Elab_Term_Quotation_mkTuple___closed__11;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Lean_Elab_Term_Quotation_mkTuple___closed__12;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/Quotation/Util.c generated
View file

@ -578,7 +578,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Syntax_instForInTopDownSyntax_loop___at_Lean_Elab_Term_Quotation_getAntiquotationIds___spec__2___closed__4;
x_2 = l_Lean_Syntax_instForInTopDownSyntax_loop___at_Lean_Elab_Term_Quotation_getAntiquotationIds___spec__2___closed__5;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Lean_Syntax_instForInTopDownSyntax_loop___at_Lean_Elab_Term_Quotation_getAntiquotationIds___spec__2___closed__6;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

498
stage0/stdlib/Lean/Elab/StructInst.c generated
View file

@ -81,7 +81,6 @@ lean_object* lean_array_uget(lean_object*, size_t);
LEAN_EXPORT lean_object* l_Lean_Elab_throwAbortTerm___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_expandNonAtomicExplicitSources___spec__2___rarg(lean_object*);
static lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabModifyOp___lambda__2___closed__2;
LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Elab_Term_StructInst_formatStruct___spec__1(lean_object*, lean_object*);
lean_object* lean_expr_update_mdata(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_StructInst_expandStructInstFieldAbbrev___lambda__1___closed__8;
lean_object* l_Array_append___rarg(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_StructInst_elabStructInst___closed__3;
@ -134,6 +133,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Term_StructInst_expandStructInstExp
LEAN_EXPORT lean_object* l_Lean_Elab_Term_StructInst_DefaultFields_mkDefaultValueAux_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_StructInst_expandStructInstExpectedType___closed__20;
lean_object* l_Lean_Expr_mdata___override(lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkCtorHeaderAux___closed__1;
LEAN_EXPORT lean_object* l_Lean_markUsedAssignment___at_Lean_Elab_Term_StructInst_DefaultFields_step___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_StructInst_expandStructInstFieldAbbrev___lambda__1___closed__2;
@ -506,7 +506,6 @@ lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Term_StructInst_Struct_structName___boxed(lean_object*);
static lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabModifyOp___lambda__3___closed__8;
LEAN_EXPORT lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Elab_Term_StructInst_DefaultFields_propagateLoop___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_update_proj(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_StructInst_instInhabitedField___closed__1;
static lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabModifyOp___lambda__3___closed__4;
static lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabModifyOp___lambda__2___closed__7;
@ -545,6 +544,7 @@ static lean_object* l_Lean_Elab_Term_StructInst_expandStructInstExpectedType___c
LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStructInstAux___spec__1___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Term_StructInst_elabStructInst___closed__2;
static lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabModifyOp___lambda__3___closed__2;
size_t lean_ptr_addr(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_isModifyOp_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStruct(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_StructInst_expandStructInstExpectedType___closed__2;
@ -706,6 +706,7 @@ extern lean_object* l_Lean_Elab_unsupportedSyntaxExceptionId;
LEAN_EXPORT lean_object* l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_getStructName___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_findField_x3f(lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_StructInst_expandStructInstFieldAbbrev___spec__2___closed__4;
lean_object* l_Lean_Expr_proj___override(lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_isModifyOp_x3f___spec__3___closed__5;
lean_object* l_ReaderT_instMonadReaderT___rarg(lean_object*);
static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_elabStructInstAux___spec__5___rarg___closed__2;
@ -3441,7 +3442,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkSourcesWithSyntax___closed__1;
x_2 = l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkSourcesWithSyntax___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l___private_Lean_Elab_StructInst_0__Lean_Elab_Term_StructInst_mkSourcesWithSyntax___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -21386,248 +21387,373 @@ return x_81;
}
case 10:
{
lean_object* x_82; lean_object* x_83;
x_82 = lean_ctor_get(x_2, 1);
lean_object* x_82; lean_object* x_83; lean_object* x_84;
x_82 = lean_ctor_get(x_2, 0);
lean_inc(x_82);
x_83 = l_Lean_Elab_Term_StructInst_DefaultFields_reduce(x_1, x_82, x_3, x_4, x_5, x_6, x_7);
if (lean_obj_tag(x_83) == 0)
x_83 = lean_ctor_get(x_2, 1);
lean_inc(x_83);
lean_inc(x_83);
x_84 = l_Lean_Elab_Term_StructInst_DefaultFields_reduce(x_1, x_83, x_3, x_4, x_5, x_6, x_7);
if (lean_obj_tag(x_84) == 0)
{
uint8_t x_84;
x_84 = !lean_is_exclusive(x_83);
if (x_84 == 0)
uint8_t x_85;
x_85 = !lean_is_exclusive(x_84);
if (x_85 == 0)
{
lean_object* x_85; lean_object* x_86;
x_85 = lean_ctor_get(x_83, 0);
x_86 = l_Lean_Elab_Term_StructInst_defaultMissing_x3f(x_2);
if (lean_obj_tag(x_86) == 0)
lean_object* x_86; lean_object* x_87;
x_86 = lean_ctor_get(x_84, 0);
x_87 = l_Lean_Elab_Term_StructInst_defaultMissing_x3f(x_2);
if (lean_obj_tag(x_87) == 0)
{
lean_object* x_87;
x_87 = lean_expr_update_mdata(x_2, x_85);
lean_ctor_set(x_83, 0, x_87);
return x_83;
}
else
{
uint8_t x_88;
lean_dec(x_86);
x_88 = l_Lean_Expr_isMVar(x_85);
if (x_88 == 0)
{
lean_dec(x_2);
return x_83;
}
else
{
lean_object* x_89;
x_89 = lean_expr_update_mdata(x_2, x_85);
lean_ctor_set(x_83, 0, x_89);
return x_83;
}
}
}
else
{
lean_object* x_90; lean_object* x_91; lean_object* x_92;
x_90 = lean_ctor_get(x_83, 0);
x_91 = lean_ctor_get(x_83, 1);
lean_inc(x_91);
lean_inc(x_90);
size_t x_88; size_t x_89; uint8_t x_90;
x_88 = lean_ptr_addr(x_83);
lean_dec(x_83);
x_92 = l_Lean_Elab_Term_StructInst_defaultMissing_x3f(x_2);
if (lean_obj_tag(x_92) == 0)
x_89 = lean_ptr_addr(x_86);
x_90 = lean_usize_dec_eq(x_88, x_89);
if (x_90 == 0)
{
lean_object* x_93; lean_object* x_94;
x_93 = lean_expr_update_mdata(x_2, x_90);
x_94 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_94, 0, x_93);
lean_ctor_set(x_94, 1, x_91);
return x_94;
lean_object* x_91;
lean_dec(x_2);
x_91 = l_Lean_Expr_mdata___override(x_82, x_86);
lean_ctor_set(x_84, 0, x_91);
return x_84;
}
else
{
uint8_t x_95;
lean_dec(x_92);
x_95 = l_Lean_Expr_isMVar(x_90);
lean_dec(x_86);
lean_dec(x_82);
lean_ctor_set(x_84, 0, x_2);
return x_84;
}
}
else
{
uint8_t x_92;
lean_dec(x_87);
x_92 = l_Lean_Expr_isMVar(x_86);
if (x_92 == 0)
{
lean_dec(x_83);
lean_dec(x_82);
lean_dec(x_2);
return x_84;
}
else
{
size_t x_93; size_t x_94; uint8_t x_95;
x_93 = lean_ptr_addr(x_83);
lean_dec(x_83);
x_94 = lean_ptr_addr(x_86);
x_95 = lean_usize_dec_eq(x_93, x_94);
if (x_95 == 0)
{
lean_object* x_96;
lean_dec(x_2);
x_96 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_96, 0, x_90);
lean_ctor_set(x_96, 1, x_91);
return x_96;
x_96 = l_Lean_Expr_mdata___override(x_82, x_86);
lean_ctor_set(x_84, 0, x_96);
return x_84;
}
else
{
lean_object* x_97; lean_object* x_98;
x_97 = lean_expr_update_mdata(x_2, x_90);
x_98 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_98, 0, x_97);
lean_ctor_set(x_98, 1, x_91);
return x_98;
lean_dec(x_86);
lean_dec(x_82);
lean_ctor_set(x_84, 0, x_2);
return x_84;
}
}
}
}
else
{
uint8_t x_99;
lean_dec(x_2);
x_99 = !lean_is_exclusive(x_83);
if (x_99 == 0)
lean_object* x_97; lean_object* x_98; lean_object* x_99;
x_97 = lean_ctor_get(x_84, 0);
x_98 = lean_ctor_get(x_84, 1);
lean_inc(x_98);
lean_inc(x_97);
lean_dec(x_84);
x_99 = l_Lean_Elab_Term_StructInst_defaultMissing_x3f(x_2);
if (lean_obj_tag(x_99) == 0)
{
return x_83;
}
else
{
lean_object* x_100; lean_object* x_101; lean_object* x_102;
x_100 = lean_ctor_get(x_83, 0);
x_101 = lean_ctor_get(x_83, 1);
lean_inc(x_101);
lean_inc(x_100);
size_t x_100; size_t x_101; uint8_t x_102;
x_100 = lean_ptr_addr(x_83);
lean_dec(x_83);
x_102 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_102, 0, x_100);
lean_ctor_set(x_102, 1, x_101);
return x_102;
x_101 = lean_ptr_addr(x_97);
x_102 = lean_usize_dec_eq(x_100, x_101);
if (x_102 == 0)
{
lean_object* x_103; lean_object* x_104;
lean_dec(x_2);
x_103 = l_Lean_Expr_mdata___override(x_82, x_97);
x_104 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_104, 0, x_103);
lean_ctor_set(x_104, 1, x_98);
return x_104;
}
else
{
lean_object* x_105;
lean_dec(x_97);
lean_dec(x_82);
x_105 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_105, 0, x_2);
lean_ctor_set(x_105, 1, x_98);
return x_105;
}
}
else
{
uint8_t x_106;
lean_dec(x_99);
x_106 = l_Lean_Expr_isMVar(x_97);
if (x_106 == 0)
{
lean_object* x_107;
lean_dec(x_83);
lean_dec(x_82);
lean_dec(x_2);
x_107 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_107, 0, x_97);
lean_ctor_set(x_107, 1, x_98);
return x_107;
}
else
{
size_t x_108; size_t x_109; uint8_t x_110;
x_108 = lean_ptr_addr(x_83);
lean_dec(x_83);
x_109 = lean_ptr_addr(x_97);
x_110 = lean_usize_dec_eq(x_108, x_109);
if (x_110 == 0)
{
lean_object* x_111; lean_object* x_112;
lean_dec(x_2);
x_111 = l_Lean_Expr_mdata___override(x_82, x_97);
x_112 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_112, 0, x_111);
lean_ctor_set(x_112, 1, x_98);
return x_112;
}
else
{
lean_object* x_113;
lean_dec(x_97);
lean_dec(x_82);
x_113 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_113, 0, x_2);
lean_ctor_set(x_113, 1, x_98);
return x_113;
}
}
}
}
}
else
{
uint8_t x_114;
lean_dec(x_83);
lean_dec(x_82);
lean_dec(x_2);
x_114 = !lean_is_exclusive(x_84);
if (x_114 == 0)
{
return x_84;
}
else
{
lean_object* x_115; lean_object* x_116; lean_object* x_117;
x_115 = lean_ctor_get(x_84, 0);
x_116 = lean_ctor_get(x_84, 1);
lean_inc(x_116);
lean_inc(x_115);
lean_dec(x_84);
x_117 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_117, 0, x_115);
lean_ctor_set(x_117, 1, x_116);
return x_117;
}
}
}
case 11:
{
lean_object* x_103; lean_object* x_104; lean_object* x_105;
x_103 = lean_ctor_get(x_2, 1);
lean_inc(x_103);
x_104 = lean_ctor_get(x_2, 2);
lean_inc(x_104);
lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121;
x_118 = lean_ctor_get(x_2, 0);
lean_inc(x_118);
x_119 = lean_ctor_get(x_2, 1);
lean_inc(x_119);
x_120 = lean_ctor_get(x_2, 2);
lean_inc(x_120);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_104);
x_105 = l_Lean_Meta_project_x3f(x_104, x_103, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_103);
if (lean_obj_tag(x_105) == 0)
{
lean_object* x_106;
x_106 = lean_ctor_get(x_105, 0);
lean_inc(x_106);
if (lean_obj_tag(x_106) == 0)
{
lean_object* x_107; lean_object* x_108;
x_107 = lean_ctor_get(x_105, 1);
lean_inc(x_107);
lean_dec(x_105);
x_108 = l_Lean_Elab_Term_StructInst_DefaultFields_reduce(x_1, x_104, x_3, x_4, x_5, x_6, x_107);
if (lean_obj_tag(x_108) == 0)
{
uint8_t x_109;
x_109 = !lean_is_exclusive(x_108);
if (x_109 == 0)
{
lean_object* x_110; lean_object* x_111;
x_110 = lean_ctor_get(x_108, 0);
x_111 = lean_expr_update_proj(x_2, x_110);
lean_ctor_set(x_108, 0, x_111);
return x_108;
}
else
{
lean_object* x_112; lean_object* x_113; lean_object* x_114; lean_object* x_115;
x_112 = lean_ctor_get(x_108, 0);
x_113 = lean_ctor_get(x_108, 1);
lean_inc(x_113);
lean_inc(x_112);
lean_dec(x_108);
x_114 = lean_expr_update_proj(x_2, x_112);
x_115 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_115, 0, x_114);
lean_ctor_set(x_115, 1, x_113);
return x_115;
}
}
else
{
uint8_t x_116;
lean_dec(x_2);
x_116 = !lean_is_exclusive(x_108);
if (x_116 == 0)
{
return x_108;
}
else
{
lean_object* x_117; lean_object* x_118; lean_object* x_119;
x_117 = lean_ctor_get(x_108, 0);
x_118 = lean_ctor_get(x_108, 1);
lean_inc(x_118);
lean_inc(x_117);
lean_dec(x_108);
x_119 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_119, 0, x_117);
lean_ctor_set(x_119, 1, x_118);
return x_119;
}
}
}
else
{
lean_object* x_120; lean_object* x_121;
lean_dec(x_104);
lean_dec(x_2);
x_120 = lean_ctor_get(x_105, 1);
lean_inc(x_120);
lean_dec(x_105);
x_121 = lean_ctor_get(x_106, 0);
lean_inc(x_121);
lean_dec(x_106);
x_2 = x_121;
x_7 = x_120;
x_121 = l_Lean_Meta_project_x3f(x_120, x_119, x_3, x_4, x_5, x_6, x_7);
if (lean_obj_tag(x_121) == 0)
{
lean_object* x_122;
x_122 = lean_ctor_get(x_121, 0);
lean_inc(x_122);
if (lean_obj_tag(x_122) == 0)
{
lean_object* x_123; lean_object* x_124;
x_123 = lean_ctor_get(x_121, 1);
lean_inc(x_123);
lean_dec(x_121);
lean_inc(x_120);
x_124 = l_Lean_Elab_Term_StructInst_DefaultFields_reduce(x_1, x_120, x_3, x_4, x_5, x_6, x_123);
if (lean_obj_tag(x_124) == 0)
{
uint8_t x_125;
x_125 = !lean_is_exclusive(x_124);
if (x_125 == 0)
{
lean_object* x_126; size_t x_127; size_t x_128; uint8_t x_129;
x_126 = lean_ctor_get(x_124, 0);
x_127 = lean_ptr_addr(x_120);
lean_dec(x_120);
x_128 = lean_ptr_addr(x_126);
x_129 = lean_usize_dec_eq(x_127, x_128);
if (x_129 == 0)
{
lean_object* x_130;
lean_dec(x_2);
x_130 = l_Lean_Expr_proj___override(x_118, x_119, x_126);
lean_ctor_set(x_124, 0, x_130);
return x_124;
}
else
{
lean_dec(x_126);
lean_dec(x_119);
lean_dec(x_118);
lean_ctor_set(x_124, 0, x_2);
return x_124;
}
}
else
{
lean_object* x_131; lean_object* x_132; size_t x_133; size_t x_134; uint8_t x_135;
x_131 = lean_ctor_get(x_124, 0);
x_132 = lean_ctor_get(x_124, 1);
lean_inc(x_132);
lean_inc(x_131);
lean_dec(x_124);
x_133 = lean_ptr_addr(x_120);
lean_dec(x_120);
x_134 = lean_ptr_addr(x_131);
x_135 = lean_usize_dec_eq(x_133, x_134);
if (x_135 == 0)
{
lean_object* x_136; lean_object* x_137;
lean_dec(x_2);
x_136 = l_Lean_Expr_proj___override(x_118, x_119, x_131);
x_137 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_137, 0, x_136);
lean_ctor_set(x_137, 1, x_132);
return x_137;
}
else
{
lean_object* x_138;
lean_dec(x_131);
lean_dec(x_119);
lean_dec(x_118);
x_138 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_138, 0, x_2);
lean_ctor_set(x_138, 1, x_132);
return x_138;
}
}
}
else
{
uint8_t x_139;
lean_dec(x_120);
lean_dec(x_119);
lean_dec(x_118);
lean_dec(x_2);
x_139 = !lean_is_exclusive(x_124);
if (x_139 == 0)
{
return x_124;
}
else
{
lean_object* x_140; lean_object* x_141; lean_object* x_142;
x_140 = lean_ctor_get(x_124, 0);
x_141 = lean_ctor_get(x_124, 1);
lean_inc(x_141);
lean_inc(x_140);
lean_dec(x_124);
x_142 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_142, 0, x_140);
lean_ctor_set(x_142, 1, x_141);
return x_142;
}
}
}
else
{
lean_object* x_143; lean_object* x_144;
lean_dec(x_120);
lean_dec(x_119);
lean_dec(x_118);
lean_dec(x_2);
x_143 = lean_ctor_get(x_121, 1);
lean_inc(x_143);
lean_dec(x_121);
x_144 = lean_ctor_get(x_122, 0);
lean_inc(x_144);
lean_dec(x_122);
x_2 = x_144;
x_7 = x_143;
goto _start;
}
}
else
{
uint8_t x_123;
lean_dec(x_104);
uint8_t x_146;
lean_dec(x_120);
lean_dec(x_119);
lean_dec(x_118);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_123 = !lean_is_exclusive(x_105);
if (x_123 == 0)
x_146 = !lean_is_exclusive(x_121);
if (x_146 == 0)
{
return x_105;
return x_121;
}
else
{
lean_object* x_124; lean_object* x_125; lean_object* x_126;
x_124 = lean_ctor_get(x_105, 0);
x_125 = lean_ctor_get(x_105, 1);
lean_inc(x_125);
lean_inc(x_124);
lean_dec(x_105);
x_126 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_126, 0, x_124);
lean_ctor_set(x_126, 1, x_125);
return x_126;
lean_object* x_147; lean_object* x_148; lean_object* x_149;
x_147 = lean_ctor_get(x_121, 0);
x_148 = lean_ctor_get(x_121, 1);
lean_inc(x_148);
lean_inc(x_147);
lean_dec(x_121);
x_149 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_149, 0, x_147);
lean_ctor_set(x_149, 1, x_148);
return x_149;
}
}
}
default:
{
lean_object* x_127;
lean_object* x_150;
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_127 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_127, 0, x_2);
lean_ctor_set(x_127, 1, x_7);
return x_127;
x_150 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_150, 0, x_2);
lean_ctor_set(x_150, 1, x_7);
return x_150;
}
}
}

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

File diff suppressed because it is too large Load diff

2
stage0/stdlib/Lean/Elab/Syntax.c generated
View file

@ -1369,7 +1369,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Term_mkParserSeq___closed__4;
x_2 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Term_mkParserSeq___closed__5;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l___private_Lean_Elab_Syntax_0__Lean_Elab_Term_mkParserSeq___closed__6;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Elab/SyntheticMVars.c generated
View file

@ -6491,7 +6491,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeUsingDefaultPrio_synthesizeUsingDefaultInstance___spec__1___closed__1;
x_2 = l_Std_Range_forIn_loop___at___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeUsingDefaultPrio_synthesizeUsingDefaultInstance___spec__1___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeUsingDefaultPrio_synthesizeUsingDefaultInstance___spec__1___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2706
stage0/stdlib/Lean/Elab/Tactic/Basic.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -66,7 +66,6 @@ static lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_evalOpen__
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalIntros_declRange___closed__2;
lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalRotateRight(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_insert___at_Lean_NameSet_insert___spec__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_ContextInfo_saveNoFileMap___at_Lean_Elab_Tactic_renameInaccessibles___spec__5___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalTacticSeq1Indented(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -160,7 +159,6 @@ LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDbgTrace(lean_objec
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDone___closed__5;
static lean_object* l_Lean_Elab_Tactic_evalCase___closed__1;
static lean_object* l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_resolveNameUsingNamespacesCore___at_Lean_Elab_Tactic_evalOpen___spec__22___closed__3;
lean_object* l_Lean_Elab_Tactic_evalTacticAux(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_resolveGlobalConstCore___at_Lean_Elab_Tactic_evalOpen___spec__11___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* l_Lean_Elab_Tactic_done(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_evalOpen___spec__18___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -508,7 +506,6 @@ LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDone(lean_object*);
static lean_object* l_Lean_Elab_nestedExceptionToMessageData___at_Lean_Elab_Tactic_evalOpen___spec__25___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalFocus___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalFailIfSuccess_declRange___closed__2;
lean_object* l_Lean_Elab_withInfoTreeContext___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_getUnsolvedGoals(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Open_0__Lean_Elab_OpenDecl_elabOpenScoped___at_Lean_Elab_Tactic_evalOpen___spec__29(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___regBuiltin_Lean_Elab_Tactic_evalOpen_declRange___closed__4;
@ -550,7 +547,6 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalAssumption___closed__1;
static lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_evalOpen___spec__2___closed__7;
lean_object* lean_st_mk_ref(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSubstVars___closed__3;
lean_object* l_Lean_throwError___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoTreeContext___at_Lean_Elab_Term_runTactic___spec__9(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___regBuiltin_Lean_Elab_Tactic_evalDone___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTraceState_declRange___closed__2;
@ -575,7 +571,6 @@ lean_object* l_Array_back___rarg(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_ContextInfo_saveNoFileMap___at_Lean_Elab_Tactic_renameInaccessibles___spec__5___rarg___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalSleep(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRefl___closed__1;
lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_refineCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRenameInaccessibles_declRange___closed__3;
static lean_object* l_Lean_Elab_Tactic_evalIntro___closed__26;
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Tactic_addCheckpoints___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*);
@ -726,8 +721,10 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalAssumption___boxed(lean_object*)
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalFirst_loop___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_Lean_Elab_elabSetOption___at_Lean_Elab_Tactic_elabSetOption___spec__1___closed__4;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_forEachVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_addCheckpoints_push___closed__10;
lean_object* l_ReaderT_pure___at_Lean_Elab_Tactic_saveTacticInfoForToken___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic_throwExs___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalRevert(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalFocus(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_Elab_Tactic_evalWithAnnotateState___closed__1;
@ -825,6 +822,7 @@ lean_object* l_Lean_Syntax_getArgs(lean_object*);
lean_object* l_Lean_Name_append(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalRotateLeft(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___regBuiltin_Lean_Elab_Tactic_evalParen_declRange(lean_object*);
lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Tactic_evalTactic_expandEval___spec__1(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_Std_Range_forIn_loop___at_Lean_Elab_Tactic_renameInaccessibles___spec__1___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_evalFail___closed__8;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSubstVars___closed__1;
@ -883,6 +881,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalFail(lean_object*, lean_object*,
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalWithAnnotateState_declRange___closed__2;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Tactic_renameInaccessibles___spec__8(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_evalIntro___closed__9;
lean_object* l_Lean_Elab_withInfoTreeContext___at_Lean_Elab_Tactic_evalTactic_eval___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalFailIfSuccess(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_Elab_Tactic_evalOpen___spec__35___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_Elab_Tactic_evalWithAnnotateState___closed__7;
@ -1332,7 +1331,7 @@ lean_inc(x_21);
lean_dec(x_19);
x_22 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalWithAnnotateState___lambda__1), 11, 1);
lean_closure_set(x_22, 0, x_20);
x_23 = l_Lean_Elab_withInfoTreeContext___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___spec__3(x_18, x_22, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_21);
x_23 = l_Lean_Elab_withInfoTreeContext___at_Lean_Elab_Tactic_evalTactic_eval___spec__1(x_18, x_22, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_21);
return x_23;
}
}
@ -1535,6 +1534,7 @@ _start:
lean_object* x_10;
x_10 = l_Lean_Elab_Tactic_evalDone___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_2);
lean_dec(x_1);
return x_10;
}
}
@ -1735,7 +1735,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_evalSeq1___spec__1___closed__1;
x_2 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_evalSeq1___spec__1___closed__2;
x_3 = lean_unsigned_to_nat(62u);
x_3 = lean_unsigned_to_nat(69u);
x_4 = lean_unsigned_to_nat(36u);
x_5 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_evalSeq1___spec__1___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -1910,7 +1910,7 @@ lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
x_52 = l_Lean_Elab_Tactic_evalTacticAux(x_51, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16);
x_52 = l_Lean_Elab_Tactic_evalTactic(x_51, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16);
if (lean_obj_tag(x_52) == 0)
{
lean_object* x_53; lean_object* x_54;
@ -1967,7 +1967,7 @@ lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
x_60 = l_Lean_Elab_Tactic_evalTacticAux(x_59, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16);
x_60 = l_Lean_Elab_Tactic_evalTactic(x_59, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16);
if (lean_obj_tag(x_60) == 0)
{
lean_object* x_61; lean_object* x_62;
@ -2314,7 +2314,7 @@ _start:
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = lean_unsigned_to_nat(1u);
x_12 = l_Lean_Syntax_getArg(x_1, x_11);
x_13 = l_Lean_Elab_Tactic_evalTacticAux(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_13 = l_Lean_Elab_Tactic_evalTactic(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_13;
}
}
@ -3056,7 +3056,7 @@ lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_19 = l_Lean_Elab_Tactic_evalTacticAux(x_18, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
x_19 = l_Lean_Elab_Tactic_evalTactic(x_18, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13);
if (lean_obj_tag(x_19) == 0)
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
@ -3736,7 +3736,7 @@ lean_inc(x_14);
lean_dec(x_13);
x_15 = lean_unsigned_to_nat(1u);
x_16 = l_Lean_Syntax_getArg(x_3, x_15);
x_17 = l_Lean_Elab_Tactic_evalTacticAux(x_16, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_14);
x_17 = l_Lean_Elab_Tactic_evalTactic(x_16, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_14);
return x_17;
}
else
@ -9192,7 +9192,7 @@ lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
x_31 = l_Lean_Elab_Tactic_evalTacticAux(x_19, x_2, x_3, x_4, x_5, x_6, x_7, x_30, x_9, x_17);
x_31 = l_Lean_Elab_Tactic_evalTactic(x_19, x_2, x_3, x_4, x_5, x_6, x_7, x_30, x_9, x_17);
if (lean_obj_tag(x_31) == 0)
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; uint8_t x_35;
@ -10415,7 +10415,7 @@ lean_object* x_18; lean_object* x_19; uint8_t x_20;
lean_dec(x_2);
lean_dec(x_1);
x_18 = l_Lean_Elab_elabSetOption_setOption___at_Lean_Elab_Tactic_elabSetOption___spec__6___closed__2;
x_19 = l_Lean_throwError___at_Lean_Elab_Tactic_refineCore___spec__1(x_18, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_15);
x_19 = l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic___spec__2(x_18, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_15);
lean_dec(x_10);
lean_dec(x_9);
lean_dec(x_8);
@ -10749,7 +10749,7 @@ x_23 = l_Lean_Elab_Tactic_elabSetOption___closed__1;
x_24 = l_Lean_Option_get___at_Std_Format_pretty_x27___spec__1(x_16, x_23);
lean_ctor_set(x_8, 4, x_24);
lean_ctor_set(x_8, 2, x_16);
x_25 = l_Lean_Elab_Tactic_evalTacticAux(x_19, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_17);
x_25 = l_Lean_Elab_Tactic_evalTactic(x_19, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_17);
return x_25;
}
else
@ -10788,7 +10788,7 @@ lean_ctor_set(x_37, 7, x_31);
lean_ctor_set(x_37, 8, x_32);
lean_ctor_set(x_37, 9, x_33);
lean_ctor_set(x_37, 10, x_34);
x_38 = l_Lean_Elab_Tactic_evalTacticAux(x_19, x_2, x_3, x_4, x_5, x_6, x_7, x_37, x_9, x_17);
x_38 = l_Lean_Elab_Tactic_evalTactic(x_19, x_2, x_3, x_4, x_5, x_6, x_7, x_37, x_9, x_17);
return x_38;
}
}
@ -11135,7 +11135,7 @@ lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_47 = l_Lean_Elab_Tactic_evalTacticAux(x_25, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_28);
x_47 = l_Lean_Elab_Tactic_evalTactic(x_25, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_28);
if (lean_obj_tag(x_47) == 0)
{
lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52;
@ -11332,7 +11332,7 @@ lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_89 = l_Lean_Elab_Tactic_evalTacticAux(x_68, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_71);
x_89 = l_Lean_Elab_Tactic_evalTactic(x_68, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_71);
if (lean_obj_tag(x_89) == 0)
{
lean_object* x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94;
@ -11805,7 +11805,7 @@ lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_42 = l_Lean_Elab_Tactic_evalTacticAux(x_38, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_41);
x_42 = l_Lean_Elab_Tactic_evalTactic(x_38, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_41);
if (lean_obj_tag(x_42) == 0)
{
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; uint8_t x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51;
@ -11911,7 +11911,7 @@ lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_73 = l_Lean_Elab_Tactic_evalTacticAux(x_69, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_72);
x_73 = l_Lean_Elab_Tactic_evalTactic(x_69, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_72);
if (lean_obj_tag(x_73) == 0)
{
lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; uint8_t x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83;
@ -12070,7 +12070,7 @@ lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_120 = l_Lean_Elab_Tactic_evalTacticAux(x_116, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_119);
x_120 = l_Lean_Elab_Tactic_evalTactic(x_116, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_119);
if (lean_obj_tag(x_120) == 0)
{
lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; uint8_t x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130;
@ -12259,7 +12259,7 @@ x_20 = lean_ctor_get(x_16, 1);
lean_inc(x_20);
lean_dec(x_16);
x_21 = l_Lean_Elab_Tactic_evalAnyGoals___closed__3;
x_22 = l_Lean_throwError___at_Lean_Elab_Tactic_refineCore___spec__1(x_21, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_20);
x_22 = l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic___spec__2(x_21, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_20);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
@ -12500,7 +12500,7 @@ _start:
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = lean_unsigned_to_nat(0u);
x_12 = l_Lean_Syntax_getArg(x_1, x_11);
x_13 = l_Lean_Elab_Tactic_evalTacticAux(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_13 = l_Lean_Elab_Tactic_evalTactic(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_13;
}
}
@ -12719,7 +12719,7 @@ lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_19 = l_Lean_Elab_Tactic_evalTacticAux(x_15, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_18);
x_19 = l_Lean_Elab_Tactic_evalTactic(x_15, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_18);
if (lean_obj_tag(x_19) == 0)
{
lean_dec(x_17);
@ -13474,7 +13474,7 @@ lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
x_23 = l_Lean_Elab_Tactic_evalTacticAux(x_19, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_22);
x_23 = l_Lean_Elab_Tactic_evalTactic(x_19, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_22);
if (lean_obj_tag(x_23) == 0)
{
lean_object* x_24; uint8_t x_25;
@ -13525,7 +13525,7 @@ else
{
lean_object* x_15; lean_object* x_16;
x_15 = l_Lean_Elab_Tactic_evalFailIfSuccess___closed__2;
x_16 = l_Lean_throwError___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___spec__2(x_15, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_12);
x_16 = l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic_throwExs___spec__2(x_15, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_12);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
@ -14107,7 +14107,7 @@ _start:
{
lean_object* x_10; lean_object* x_11;
x_10 = l_Lean_Elab_throwIllFormedSyntax___at_Lean_Elab_Tactic_evalTraceMessage___spec__1___closed__2;
x_11 = l_Lean_throwError___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___spec__2(x_10, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
x_11 = l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic_throwExs___spec__2(x_10, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
return x_11;
}
}
@ -16209,7 +16209,7 @@ x_58 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_58, 0, x_26);
lean_ctor_set(x_58, 1, x_57);
lean_ctor_set(x_58, 2, x_56);
x_59 = l_Lean_Elab_Tactic_evalTacticAux(x_58, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_34);
x_59 = l_Lean_Elab_Tactic_evalTactic(x_58, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_34);
return x_59;
}
}
@ -16448,7 +16448,7 @@ x_175 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_175, 0, x_83);
lean_ctor_set(x_175, 1, x_174);
lean_ctor_set(x_175, 2, x_173);
x_176 = l_Lean_Elab_Tactic_evalTacticAux(x_175, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_71);
x_176 = l_Lean_Elab_Tactic_evalTactic(x_175, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_71);
return x_176;
}
else
@ -16668,7 +16668,7 @@ x_15 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_13);
lean_ctor_set(x_5, 2, x_15);
x_16 = l_Lean_Elab_Tactic_evalTacticAux(x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
x_16 = l_Lean_Elab_Tactic_evalTactic(x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
return x_16;
}
else
@ -16723,7 +16723,7 @@ lean_ctor_set_uint8(x_35, sizeof(void*)*8 + 4, x_28);
lean_ctor_set_uint8(x_35, sizeof(void*)*8 + 5, x_29);
lean_ctor_set_uint8(x_35, sizeof(void*)*8 + 6, x_30);
lean_ctor_set_uint8(x_35, sizeof(void*)*8 + 7, x_32);
x_36 = l_Lean_Elab_Tactic_evalTacticAux(x_2, x_3, x_4, x_35, x_6, x_7, x_8, x_9, x_10, x_11);
x_36 = l_Lean_Elab_Tactic_evalTactic(x_2, x_3, x_4, x_35, x_6, x_7, x_8, x_9, x_10, x_11);
return x_36;
}
}
@ -16746,7 +16746,7 @@ lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
x_14 = l_Lean_Elab_liftMacroM___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__1(x_13, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_14 = l_Lean_Elab_liftMacroM___at_Lean_Elab_Tactic_evalTactic_expandEval___spec__1(x_13, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
@ -26193,7 +26193,7 @@ x_42 = l_Std_Range_forIn_loop___at_Lean_Elab_Tactic_evalSeq1___spec__1___closed_
x_43 = l_panic___at_Lean_expandExplicitBindersAux_loop___spec__1(x_42);
x_44 = l_Lean_Syntax_getArg(x_43, x_13);
lean_dec(x_43);
x_45 = l_Lean_Elab_Tactic_evalTacticAux(x_44, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
x_45 = l_Lean_Elab_Tactic_evalTactic(x_44, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
return x_45;
}
else
@ -26203,7 +26203,7 @@ x_46 = lean_array_fget(x_1, x_2);
lean_dec(x_2);
x_47 = l_Lean_Syntax_getArg(x_46, x_13);
lean_dec(x_46);
x_48 = l_Lean_Elab_Tactic_evalTacticAux(x_47, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
x_48 = l_Lean_Elab_Tactic_evalTactic(x_47, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
return x_48;
}
}
@ -26673,7 +26673,7 @@ lean_ctor_set(x_37, 1, x_17);
x_38 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_38, 0, x_37);
lean_ctor_set(x_38, 1, x_33);
x_39 = l_Lean_throwError___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___spec__2(x_38, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_13);
x_39 = l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic_throwExs___spec__2(x_38, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_13);
return x_39;
}
}
@ -26690,7 +26690,7 @@ x_42 = l_Lean_Elab_nestedExceptionToMessageData___at_Lean_Elab_Tactic_evalOpen__
x_43 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_43, 0, x_41);
lean_ctor_set(x_43, 1, x_42);
x_44 = l_Lean_throwError___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___spec__2(x_43, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_13);
x_44 = l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic_throwExs___spec__2(x_43, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_13);
return x_44;
}
}

8
stage0/stdlib/Lean/Elab/Tactic/Cache.c generated
View file

@ -24,7 +24,6 @@ static lean_object* l___private_Lean_Elab_Tactic_Cache_0__Lean_Elab_Tactic_dbg__
static lean_object* l_Lean_Elab_Tactic_initFn____x40_Lean_Elab_Tactic_Cache___hyg_16____closed__6;
LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_Elab_Tactic_evalCheckpoint___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_structEq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalTacticAux(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_Std_PersistentHashMap_insertAux___at_Lean_Elab_Tactic_evalCheckpoint___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*);
size_t lean_usize_sub(size_t, size_t);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCheckpoint___closed__14;
@ -32,6 +31,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCheckpoint_declRange___c
lean_object* lean_dbg_trace(lean_object*, lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Cache_0__Lean_Elab_Tactic_dbg__cache(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalTactic(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_Std_PersistentHashMap_findAtAux___at___private_Lean_Elab_Tactic_Cache_0__Lean_Elab_Tactic_dbg__cache_x27___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Cache_0__Lean_Elab_Tactic_dbg__cache___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalCheckpoint___closed__5;
@ -1917,7 +1917,7 @@ lean_inc(x_13);
lean_dec(x_11);
x_14 = lean_unsigned_to_nat(1u);
x_15 = l_Lean_Syntax_getArg(x_1, x_14);
x_16 = l_Lean_Elab_Tactic_evalTacticAux(x_15, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_13);
x_16 = l_Lean_Elab_Tactic_evalTactic(x_15, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_13);
return x_16;
}
else
@ -1940,7 +1940,7 @@ lean_dec(x_19);
lean_dec(x_17);
x_22 = lean_unsigned_to_nat(1u);
x_23 = l_Lean_Syntax_getArg(x_1, x_22);
x_24 = l_Lean_Elab_Tactic_evalTacticAux(x_23, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_18);
x_24 = l_Lean_Elab_Tactic_evalTactic(x_23, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_18);
return x_24;
}
else
@ -1983,7 +1983,7 @@ lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
lean_inc(x_27);
x_31 = l_Lean_Elab_Tactic_evalTacticAux(x_27, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_30);
x_31 = l_Lean_Elab_Tactic_evalTactic(x_27, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_30);
if (lean_obj_tag(x_31) == 0)
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53;

25
stage0/stdlib/Lean/Elab/Tactic/Conv/Basic.c generated
View file

@ -70,7 +70,6 @@ lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalExact_
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalZeta___closed__3;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalReduce_declRange___closed__3;
lean_object* l_Lean_mkLHSGoal(lean_object*);
lean_object* l_Lean_Elab_Tactic_evalTacticAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalNestedTactic___closed__4;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalNestedTacticCore_declRange___closed__1;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalParen___closed__3;
@ -202,7 +201,6 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalNestedConv___closed
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Conv_markAsConvGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalWhnf___closed__9;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalZeta___closed__1;
lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_refineCore___spec__1(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_Elab_Tactic_Conv_evalConvSeqBracketed___lambda__2___closed__3;
lean_object* l_Lean_addBuiltinDeclarationRanges(lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalConvSeqBracketed_declRange___closed__5;
@ -251,6 +249,7 @@ lean_object* l_Lean_LocalDecl_fvarId(lean_object*);
static lean_object* l_List_forIn_loop___at_Lean_Elab_Tactic_Conv_convert___spec__1___closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Conv_Basic_0__Lean_Elab_Tactic_Conv_convLocalDecl___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Conv_evalConvSeqBracketed___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalConvSeqBracketed___lambda__2___closed__25;
lean_object* l_ReaderT_pure___at_Lean_Elab_Tactic_saveTacticInfoForToken___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalWhnf_declRange___closed__2;
@ -941,7 +940,7 @@ x_71 = l_Lean_Elab_Tactic_Conv_convert___closed__5;
x_72 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_72, 0, x_70);
lean_ctor_set(x_72, 1, x_71);
x_73 = l_Lean_throwError___at_Lean_Elab_Tactic_refineCore___spec__1(x_72, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_67);
x_73 = l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic___spec__2(x_72, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_67);
x_74 = lean_ctor_get(x_73, 0);
lean_inc(x_74);
x_75 = lean_ctor_get(x_73, 1);
@ -3660,7 +3659,7 @@ x_85 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_85, 0, x_34);
lean_ctor_set(x_85, 1, x_84);
lean_ctor_set(x_85, 2, x_83);
x_86 = l_Lean_Elab_Tactic_evalTacticAux(x_85, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_23);
x_86 = l_Lean_Elab_Tactic_evalTactic(x_85, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_23);
return x_86;
}
else
@ -4165,7 +4164,7 @@ _start:
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = lean_unsigned_to_nat(0u);
x_12 = l_Lean_Syntax_getArg(x_1, x_11);
x_13 = l_Lean_Elab_Tactic_evalTacticAux(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_13 = l_Lean_Elab_Tactic_evalTactic(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_13;
}
}
@ -4635,7 +4634,7 @@ _start:
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = lean_unsigned_to_nat(1u);
x_12 = l_Lean_Syntax_getArg(x_1, x_11);
x_13 = l_Lean_Elab_Tactic_evalTacticAux(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_13 = l_Lean_Elab_Tactic_evalTactic(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_13;
}
}
@ -5340,7 +5339,7 @@ lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
x_13 = l_Lean_Elab_Tactic_evalTacticAux(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_13 = l_Lean_Elab_Tactic_evalTactic(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15;
@ -5561,7 +5560,7 @@ lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
x_11 = l_Lean_Elab_Tactic_evalTacticAux(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_11 = l_Lean_Elab_Tactic_evalTactic(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13;
@ -6256,7 +6255,7 @@ x_57 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_57, 0, x_36);
lean_ctor_set(x_57, 1, x_56);
lean_ctor_set(x_57, 2, x_55);
x_58 = l_Lean_Elab_Tactic_evalTacticAux(x_57, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_29);
x_58 = l_Lean_Elab_Tactic_evalTactic(x_57, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_29);
return x_58;
}
else
@ -6968,7 +6967,7 @@ x_125 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_125, 0, x_79);
lean_ctor_set(x_125, 1, x_4);
lean_ctor_set(x_125, 2, x_124);
x_126 = l_Lean_Elab_Tactic_evalTacticAux(x_125, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_68);
x_126 = l_Lean_Elab_Tactic_evalTactic(x_125, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_68);
return x_126;
}
else
@ -6988,7 +6987,7 @@ x_132 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_132, 0, x_79);
lean_ctor_set(x_132, 1, x_4);
lean_ctor_set(x_132, 2, x_131);
x_133 = l_Lean_Elab_Tactic_evalTacticAux(x_132, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_68);
x_133 = l_Lean_Elab_Tactic_evalTactic(x_132, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_68);
return x_133;
}
}
@ -7026,7 +7025,7 @@ x_148 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_148, 0, x_79);
lean_ctor_set(x_148, 1, x_4);
lean_ctor_set(x_148, 2, x_147);
x_149 = l_Lean_Elab_Tactic_evalTacticAux(x_148, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_68);
x_149 = l_Lean_Elab_Tactic_evalTactic(x_148, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_68);
return x_149;
}
else
@ -7046,7 +7045,7 @@ x_155 = lean_alloc_ctor(1, 3, 0);
lean_ctor_set(x_155, 0, x_79);
lean_ctor_set(x_155, 1, x_4);
lean_ctor_set(x_155, 2, x_154);
x_156 = l_Lean_Elab_Tactic_evalTacticAux(x_155, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_68);
x_156 = l_Lean_Elab_Tactic_evalTactic(x_155, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_68);
return x_156;
}
}

4
stage0/stdlib/Lean/Elab/Tactic/Conv/Change.c generated
View file

@ -35,7 +35,6 @@ lean_object* l_Lean_Elab_Tactic_filterOldMVars(lean_object*, lean_object*, lean_
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__12;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange_declRange___closed__3;
lean_object* l_Lean_Meta_isExprDefEqGuarded(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_refineCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addBuiltinDeclarationRanges(lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange_declRange___closed__5;
static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__1;
@ -43,6 +42,7 @@ static lean_object* l_Lean_Elab_Tactic_Conv_evalChange___closed__11;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Conv_evalChange___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_getLhs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Tactic_tacticElabAttribute;
lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange___closed__6;
lean_object* l_Lean_Elab_Tactic_elabTermEnsuringType(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalChange_declRange___closed__7;
@ -372,7 +372,7 @@ x_53 = l_Lean_Elab_Tactic_Conv_evalChange___closed__16;
x_54 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_54, 0, x_52);
lean_ctor_set(x_54, 1, x_53);
x_55 = l_Lean_throwError___at_Lean_Elab_Tactic_refineCore___spec__1(x_54, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_45);
x_55 = l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic___spec__2(x_54, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_45);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);

10
stage0/stdlib/Lean/Elab/Tactic/Conv/Congr.c generated
View file

@ -146,7 +146,6 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalLhs_declRange___clo
lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*);
lean_object* l_Nat_repr(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Conv_evalLhs___boxed(lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_extLetBodyCongr_x3f___lambda__3___closed__6;
lean_object* l_Lean_Syntax_getId(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Conv_evalArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -157,7 +156,6 @@ static lean_object* l___private_Lean_Elab_Tactic_Conv_Congr_0__Lean_Elab_Tactic_
lean_object* l_Lean_Expr_sort___override(lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_markAsConvGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Conv_extLetBodyCongr_x3f___lambda__5(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_throwError___at_Lean_Elab_Tactic_refineCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addBuiltinDeclarationRanges(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_extLetBodyCongr_x3f___lambda__3___closed__3;
lean_object* lean_array_to_list(lean_object*, lean_object*);
@ -190,8 +188,10 @@ extern lean_object* l_Lean_Elab_Tactic_tacticElabAttribute;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_Conv_extLetBodyCongr_x3f___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Tactic_Conv_Congr_0__Lean_Elab_Tactic_Conv_extCore___lambda__2___closed__3;
lean_object* l_Int_toNat(lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Tactic_Conv_Congr_0__Lean_Elab_Tactic_Conv_extCore___lambda__2___closed__5;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalLhs_declRange___closed__5;
lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic_throwExs___spec__2(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___private_Lean_Elab_Tactic_Conv_Congr_0__Lean_Elab_Tactic_Conv_selectIdx___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalExt(lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalRhs___closed__2;
@ -3459,7 +3459,7 @@ x_24 = l___private_Lean_Elab_Tactic_Conv_Congr_0__Lean_Elab_Tactic_Conv_selectId
x_25 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
x_26 = l_Lean_throwError___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___spec__2(x_25, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
x_26 = l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic_throwExs___spec__2(x_25, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
return x_26;
}
}
@ -3584,7 +3584,7 @@ if (lean_obj_tag(x_28) == 0)
{
lean_object* x_29; lean_object* x_30; uint8_t x_31;
x_29 = l___private_Lean_Elab_Tactic_Conv_Congr_0__Lean_Elab_Tactic_Conv_selectIdx___closed__4;
x_30 = l_Lean_throwError___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___spec__2(x_29, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_26);
x_30 = l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic_throwExs___spec__2(x_29, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_26);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);
@ -4612,7 +4612,7 @@ lean_object* x_23; lean_object* x_24; uint8_t x_25;
lean_dec(x_18);
lean_dec(x_3);
x_23 = l_Lean_Elab_Tactic_Conv_evalArg___lambda__2___closed__4;
x_24 = l_Lean_throwError___at_Lean_Elab_Tactic_refineCore___spec__1(x_23, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
x_24 = l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic___spec__2(x_23, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_9);

4
stage0/stdlib/Lean/Elab/Tactic/Conv/Pattern.c generated
View file

@ -57,7 +57,6 @@ static lean_object* l_Lean_Elab_Tactic_Conv_evalPattern___lambda__3___closed__4;
lean_object* l_Lean_Elab_Tactic_Conv_mkConvGoalFor(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalPattern_declRange___closed__7;
lean_object* lean_st_mk_ref(lean_object*, lean_object*);
lean_object* l_Lean_throwError___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalPattern___closed__8;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_Conv_evalPattern___closed__4;
lean_object* l_Lean_Meta_isExprDefEqGuarded(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -69,6 +68,7 @@ lean_object* l_Lean_Expr_toHeadIndex(lean_object*);
lean_object* l_Lean_Elab_Tactic_Conv_getLhs(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
extern lean_object* l_Lean_Elab_Tactic_tacticElabAttribute;
lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic_throwExs___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Conv_Pattern_0__Lean_Elab_Tactic_Conv_findPattern_x3f___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Conv_Pattern_0__Lean_Elab_Tactic_Conv_findPattern_x3f___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_Conv_evalPattern___closed__3;
@ -1749,7 +1749,7 @@ x_41 = l_Lean_Elab_Tactic_Conv_evalPattern___lambda__3___closed__4;
x_42 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_42, 0, x_40);
lean_ctor_set(x_42, 1, x_41);
x_43 = l_Lean_throwError___at___private_Lean_Elab_Tactic_Basic_0__Lean_Elab_Tactic_evalTacticUsing_loop___spec__2(x_42, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_36);
x_43 = l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic_throwExs___spec__2(x_42, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_36);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);

4
stage0/stdlib/Lean/Elab/Tactic/Delta.c generated
View file

@ -63,7 +63,6 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDelta_declRange___closed
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDelta___closed__10;
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDelta___closed__3;
lean_object* lean_format_pretty(lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_refineCore___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addBuiltinDeclarationRanges(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_getMainGoal(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_deltaLocalDecl___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*);
@ -73,6 +72,7 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_evalDelta___spe
extern lean_object* l_Lean_Elab_Tactic_tacticElabAttribute;
static lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Tactic_evalDelta___spec__7___closed__1;
static lean_object* l_Lean_Elab_Tactic_deltaLocalDecl___closed__8;
lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDelta_declRange___closed__6;
static lean_object* l_Lean_Elab_Tactic_deltaLocalDecl___closed__6;
LEAN_EXPORT lean_object* l_Lean_resolveGlobalConstCore___at_Lean_Elab_Tactic_evalDelta___spec__5___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -953,7 +953,7 @@ x_16 = l_Lean_Elab_Tactic_deltaLocalDecl___closed__8;
x_17 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_17, 0, x_15);
lean_ctor_set(x_17, 1, x_16);
x_18 = l_Lean_throwError___at_Lean_Elab_Tactic_refineCore___spec__1(x_17, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_18 = l_Lean_throwError___at_Lean_Elab_Tactic_evalTactic___spec__2(x_17, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
return x_18;
}
}

741
stage0/stdlib/Lean/Elab/Tactic/ElabTerm.c generated
View file

File diff suppressed because it is too large Load diff

Some files were not shown because too many files have changed in this diff Show more