chore: update stage0

stage0/src/CMakeLists.txt

@@ -470,12 +470,6 @@ add_custom_target(leanshared ALL
   VERBATIM)
 
 if(${STAGE} GREATER 0)
-  add_custom_target(leanpkg ALL
-    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
-    DEPENDS leanshared
-    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Leanpkg
-    VERBATIM)
-
   if(NOT EXISTS ${LEAN_SOURCE_DIR}/lake/Lake.lean)
     message(FATAL_ERROR "src/lake does not exist. Please check out the Lake submodule using `git submodule update --init src/lake`.")
   endif()

stage0/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean

@@ -17,12 +17,12 @@ partial def addSmartUnfoldingDefAux (preDef : PreDefinition) (recArgPos : Nat) :
   }
 where
   /--
-     Auxiliary method for annotating `match`-alternatives with `markSmartUnfoldingMatch` and `markSmartUnfoldigMatchAlt`.
+     Auxiliary method for annotating `match`-alternatives with `markSmartUnfoldingMatch` and `markSmartUnfoldingMatchAlt`.
 
      It uses the following approach:
      - Whenever it finds a `match` application `e` s.t. `recArgHasLooseBVarsAt preDef.declName recArgPos e`,
        it marks the `match` with `markSmartUnfoldingMatch`, and each alternative that does not contain a nested marked `match`
-       is marked with `markSmartUnfoldigMatchAlt`.
+       is marked with `markSmartUnfoldingMatchAlt`.
 
      Recall that the condition `recArgHasLooseBVarsAt preDef.declName recArgPos e` is the one used at `mkBRecOn`.
   -/
@@ -52,7 +52,7 @@ where
               let containsSUnfoldMatch := Option.isSome <| altBody.find? fun e => smartUnfoldingMatch? e |>.isSome
               if !containsSUnfoldMatch then
                 let altBody ← mkLambdaFVars xs[numParams:xs.size] altBody
-                let altBody := markSmartUnfoldigMatchAlt altBody
+                let altBody := markSmartUnfoldingMatchAlt altBody
                 mkLambdaFVars xs[0:numParams] altBody
               else
                 mkLambdaFVars xs altBody

stage0/src/Lean/Elab/Tactic/Match.lean

@@ -63,7 +63,7 @@ private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM
 def evalMatch : Tactic := fun stx => do
   let tag ← getMainTag
   let (matchTerm, cases) ← liftMacroM <| mkAuxiliaryMatchTerm tag stx
-  let refineMatchTerm ← `(tactic| refine $matchTerm)
+  let refineMatchTerm ← `(tactic| refine no_implicit_lambda% $matchTerm)
   let stxNew := mkNullNode (#[refineMatchTerm] ++ cases)
   withMacroExpansion stx stxNew <| evalTactic stxNew
 

stage0/src/Lean/Meta/Basic.lean

@@ -85,6 +85,8 @@ structure ParamInfo where
   binderInfo     : BinderInfo := BinderInfo.default
   hasFwdDeps     : Bool       := false
   backDeps       : Array Nat  := #[]
+  isProp         : Bool       := false
+  isDecInst      : Bool       := false
   deriving Inhabited
 
 def ParamInfo.isImplicit (p : ParamInfo) : Bool :=

stage0/src/Lean/Meta/CongrTheorems.lean

@@ -26,6 +26,11 @@ inductive CongrArgKind where
      The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : HEq a_i b_i`.
      `a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their heterogeneous equality. -/
     heq
+  | /--
+     For congr-simp theorems only.  Indicates a decidable instance argument.
+     The lemma contains two arguments [a_i : Decidable ...] [b_i : Decidable ...] -/
+    subsingletonInst
+  deriving Inhabited
 
 structure CongrTheorem where
   type     : Expr
@@ -110,4 +115,172 @@ where
 def mkHCongr (f : Expr) : MetaM CongrTheorem := do
   mkHCongrWithArity f (← getFunInfo f).getArity
 
+/--
+  Ensure that all dependencies for `congr_arg_kind::Eq` are `congr_arg_kind::Fixed`.
+-/
+private def fixKindsForDependencies (info : FunInfo) (kinds : Array CongrArgKind) : Array CongrArgKind := Id.run do
+  let mut kinds := kinds
+  for i in [:info.paramInfo.size] do
+    for j in [i+1:info.paramInfo.size] do
+      if info.paramInfo[j].backDeps.contains i then
+        if kinds[j] matches CongrArgKind.eq || kinds[j] matches CongrArgKind.fixed then
+          -- We must fix `i` because there is a `j` that depends on `i` and `j` is not cast-fixed.
+          kinds := kinds.set! i CongrArgKind.fixed
+          break
+  return kinds
+
+/--
+  (Try to) cast expression `e` to the given type using the equations `eqs`.
+  `deps` contains the indices of the relevant equalities.
+  Remark: deps is sorted. -/
+private partial def mkCast (e : Expr) (type : Expr) (deps : Array Nat) (eqs : Array (Option Expr)) : MetaM Expr := do
+  let rec go (i : Nat) (type : Expr) : MetaM Expr := do
+     if i < deps.size then
+       match eqs[deps[i]] with
+       | none => go (i+1) type
+       | some major =>
+         let some (_, lhs, rhs) := (← inferType major).eq? | unreachable!
+         if (← dependsOn type major.fvarId!) then
+           let motive ← mkLambdaFVars #[rhs, major] type
+           let typeNew := type.replaceFVar rhs lhs |>.replaceFVar major (← mkEqRefl lhs)
+           let minor ← go (i+1) typeNew
+           mkEqRec motive minor major
+         else
+           let motive ← mkLambdaFVars #[rhs] type
+           let typeNew := type.replaceFVar rhs lhs
+           let minor ← go (i+1) typeNew
+           mkEqNDRec motive minor major
+     else
+       return e
+  go 0 type
+
+private def hasCastLike (kinds : Array CongrArgKind) : Bool :=
+  kinds.any fun kind => kind matches CongrArgKind.cast || kind matches CongrArgKind.subsingletonInst
+
+private def withNext (type : Expr) (k : Expr → Expr → MetaM α) : MetaM α := do
+  forallBoundedTelescope type (some 1) fun xs type => k xs[0] type
+
+/--
+  Create a congruence theorem that is useful for the simplifier.
+-/
+partial def mkCongrSimpWithArity? (f : Expr) (numArgs : Nat) : MetaM (Option CongrTheorem) := do
+  let info ← getFunInfo f
+  let kinds := getKinds info
+  if let some result ← mk? f info kinds then
+    return some result
+  else if hasCastLike kinds then
+    -- Simplify kinds and try again
+    let kinds := kinds.map fun kind =>
+      if kind matches CongrArgKind.cast || kind matches CongrArgKind.subsingletonInst then CongrArgKind.fixed else kind
+    mk? f info kinds
+  else
+    return none
+where
+  /--
+    Create a congruence theorem that is useful for the simplifier.
+    In this kind of theorem, if the i-th argument is a `cast` argument, then the theorem
+    contains an input `a_i` representing the i-th argument in the left-hand-side, and
+    it appears with a cast (e.g., `Eq.drec ... a_i ...`) in the right-hand-side.
+    The idea is that the right-hand-side of this lemma "tells" the simplifier
+    how the resulting term looks like. -/
+  mk? (f : Expr) (info : FunInfo) (kinds : Array CongrArgKind) : MetaM (Option CongrTheorem) := do
+    try
+      let fType ← inferType f
+      forallBoundedTelescope fType kinds.size fun lhss xType => do
+        if lhss.size != kinds.size then return none
+        let rec go (i : Nat) (rhss : Array Expr) (eqs : Array (Option Expr)) (hyps : Array Expr) : MetaM CongrTheorem := do
+          if i == kinds.size then
+            let lhs := mkAppN f lhss
+            let rhs := mkAppN f rhss
+            let type ← mkForallFVars hyps (← mkEq lhs rhs)
+            let proof ← mkProof type kinds
+            return { type, proof, argKinds := kinds }
+          else
+            let hyps := hyps.push lhss[i]
+            match kinds[i] with
+            | CongrArgKind.heq => unreachable!
+            | CongrArgKind.fixedNoParam => unreachable!
+            | CongrArgKind.eq =>
+              let localDecl ← getLocalDecl lhss[i].fvarId!
+              withLocalDecl localDecl.userName localDecl.binderInfo localDecl.type fun rhs => do
+              withLocalDeclD ((`e).appendIndexAfter (eqs.size+1)) (← mkEq lhss[i] rhs) fun eq => do
+                go (i+1) (rhss.push rhs) (eqs.push eq) (hyps.push rhs |>.push eq)
+            | CongrArgKind.fixed => go (i+1) (rhss.push lhss[i]) (eqs.push none) hyps
+            | CongrArgKind.cast =>
+              let rhsType := (← inferType lhss[i]).replaceFVars (lhss[:rhss.size]) rhss
+              let rhs ← mkCast lhss[i] rhsType info.paramInfo[i].backDeps eqs
+              go (i+1) (rhss.push rhs) (eqs.push none) hyps
+            | CongrArgKind.subsingletonInst =>
+              let rhsType := (← inferType lhss[i]).replaceFVars (lhss[:rhss.size]) rhss
+              withLocalDecl (← getLocalDecl lhss[i].fvarId!).userName BinderInfo.instImplicit rhsType fun rhs =>
+                go (i+1) (rhss.push rhs) (eqs.push none) (hyps.push rhs)
+        return some (← go 0 #[] #[] #[])
+    catch _ =>
+      return none
+
+  mkProof (type : Expr) (kinds : Array CongrArgKind) : MetaM Expr := do
+    let rec go (i : Nat) (type : Expr) : MetaM Expr := do
+      if i == kinds.size then
+        let some (_, lhs, _) := type.eq? | unreachable!
+        mkEqRefl lhs
+      else
+        withNext type fun lhs type => do
+        match kinds[i] with
+        | CongrArgKind.heq => unreachable!
+        | CongrArgKind.fixedNoParam => unreachable!
+        | CongrArgKind.fixed => mkLambdaFVars #[lhs] (← go (i+1) type)
+        | CongrArgKind.cast => mkLambdaFVars #[lhs] (← go (i+1) type)
+        | CongrArgKind.eq =>
+          let typeSub := type.bindingBody!.bindingBody!.instantiate #[(← mkEqRefl lhs), lhs]
+          withNext type fun rhs type =>
+          withNext type fun heq type => do
+            let motive ← mkLambdaFVars #[rhs, heq] type
+            let proofSub ← go (i+1) typeSub
+            mkLambdaFVars #[lhs, rhs, heq] (← mkEqRec motive proofSub heq)
+        | CongrArgKind.subsingletonInst =>
+          let typeSub := type.bindingBody!.instantiate #[lhs]
+          withNext type fun rhs type => do
+            let motive ← mkLambdaFVars #[rhs] type
+            let proofSub ← go (i+1) typeSub
+            let heq ← mkAppM ``Subsingleton.elim #[lhs, rhs]
+            mkLambdaFVars #[lhs, rhs] (← mkEqNDRec motive proofSub heq)
+     go 0 type
+
+  getKinds (info : FunInfo) : Array CongrArgKind := Id.run do
+    /- The default `CongrArgKind` is `eq`, which allows `simp` to rewrite this
+       argument. However, if there are references from `i` to `j`, we cannot
+       rewrite both `i` and `j`. So we must change the `CongrArgKind` at
+       either `i` or `j`. In principle, if there is a dependency with `i`
+       appearing after `j`, then we set `j` to `fixed` (or `cast`). But there is
+       an optimization: if `i` is a subsingleton, we can fix it instead of
+       `j`, since all subsingletons are equal anyway. The fixing happens in
+        two loops: one for the special cases, and one for the general case. -/
+    let mut result := #[]
+    for i in [:info.paramInfo.size] do
+      if info.resultDeps.contains i then
+        result := result.push CongrArgKind.fixed
+      else if info.paramInfo[i].isProp then
+        result := result.push CongrArgKind.cast
+      else if info.paramInfo[i].isInstImplicit then
+        if shouldUseSubsingletonInst info result i then
+          result := result.push CongrArgKind.subsingletonInst
+        else
+          result := result.push CongrArgKind.fixed
+      else
+        result := result.push CongrArgKind.eq
+    return fixKindsForDependencies info result
+
+  /--
+    Test whether we should use `subsingletonInst` kind for instances which depend on `eq`.
+    (Otherwise `fixKindsForDependencies`will downgrade them to Fixed -/
+  shouldUseSubsingletonInst (info : FunInfo) (kinds : Array CongrArgKind) (i : Nat) : Bool := Id.run do
+    if info.paramInfo[i].isDecInst then
+      for j in info.paramInfo[i].backDeps do
+        if kinds[j] matches CongrArgKind.eq then
+          return true
+    return false
+
+def mkCongrSimp? (f : Expr) : MetaM (Option CongrTheorem) := do
+  mkCongrSimpWithArity? f (← getFunInfo f).getArity
+
 end Lean.Meta

stage0/src/Lean/Meta/FunInfo.lean

@@ -64,6 +64,8 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
           pinfo := pinfo.push {
             backDeps     := backDeps
             binderInfo   := decl.binderInfo
+            isProp       := (← isProp decl.type)
+            isDecInst    := (← forallTelescopeReducing decl.type fun _ type => return type.isAppOf ``Decidable)
           }
         let resultDeps := collectDeps fvars type
         pinfo := updateHasFwdDeps pinfo resultDeps

stage0/src/Lean/Meta/WHNF.lean

@@ -39,7 +39,7 @@ def smartUnfoldingMatch? (e : Expr) : Option Expr :=
   annotation? `sunfoldMatch e
 
 /-- Add auxiliary annotation to indicate expression `e` (a `match` alternative rhs) was successfully reduced by smart unfolding. -/
-def markSmartUnfoldigMatchAlt (e : Expr) : Expr :=
+def markSmartUnfoldingMatchAlt (e : Expr) : Expr :=
   mkAnnotation `sunfoldMatchAlt e
 
 def smartUnfoldingMatchAlt? (e : Expr) : Option Expr :=
@@ -472,7 +472,7 @@ partial def whnfCore (e : Expr) : MetaM Expr :=
     | _ => unreachable!
 
 /--
-  Recall that `_sunfold` auxiliary definitions contains the markers: `markSmartUnfoldigMatch` (*) and `markSmartUnfoldigMatchAlt` (**).
+  Recall that `_sunfold` auxiliary definitions contains the markers: `markSmartUnfoldingMatch` (*) and `markSmartUnfoldingMatchAlt` (**).
   For example, consider the following definition
   ```
   def r (i j : Nat) : Nat :=
@@ -496,7 +496,7 @@ partial def whnfCore (e : Expr) : MetaM Expr :=
             | Nat.succ j => (**) r i j
   ```
 
-  `match` expressions marked with `markSmartUnfoldigMatch` (*) must be reduced, otherwise the resulting term is not definitionally
+  `match` expressions marked with `markSmartUnfoldingMatch` (*) must be reduced, otherwise the resulting term is not definitionally
    equal to the given expression. The recursion may be interrupted as soon as the annotation `markSmartUnfoldingAlt` (**) is reached.
 
   For example, the term `r i j.succ.succ` reduces to the definitionally equal term `i + i * r i j`

stage0/src/Lean/Server/FileWorker.lean

@@ -182,9 +182,6 @@ section Initialization
     let stderr ← IO.ofExcept stderr.get
     match (← lakeProc.wait) with
     | 0 =>
-      -- ignore any output up to the last line
-      -- TODO: leanpkg should instead redirect nested stdout output to stderr
-      let stdout := stdout.split (· == '\n') |>.getLast!
       let Except.ok (paths : LeanPaths) ← pure (Json.parse stdout >>= fromJson?)
         | throwServerError s!"invalid output from `{cmdStr}`:\n{stdout}\nstderr:\n{stderr}"
       initSearchPath (← getBuildDir) paths.oleanPath
@@ -201,13 +198,9 @@ section Initialization
     let lakePath ← match (← IO.getEnv "LAKE") with
       | some path => pure <| System.FilePath.mk path
       | none =>
-        let lakePath :=
-          -- backward compatibility, kill when `leanpkg` is removed
-          if (← System.FilePath.pathExists "leanpkg.toml") && !(← System.FilePath.pathExists "lakefile.lean") then "leanpkg"
-          else "lake"
         let lakePath ← match (← IO.getEnv "LEAN_SYSROOT") with
-          | some path => pure <| System.FilePath.mk path / "bin" / lakePath
-          | _         => pure <| (← appDir) / lakePath
+          | some path => pure <| System.FilePath.mk path / "bin" / "lake"
+          | _         => pure <| (← appDir) / "lake"
         pure <| lakePath.withExtension System.FilePath.exeExtension
     let (headerEnv, msgLog) ← try
       if let some path := m.uri.toPath? then

stage0/src/Leanpkg/.gitignore

@@ -1 +0,0 @@
-/leanpkg/config_vars.lean

stage0/src/Leanpkg/Build.lean

@@ -1,104 +0,0 @@
-/-
-Copyright (c) 2021 Sebastian Ullrich. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich
--/
-import Lean.Data.Name
-import Lean.Elab.Import
-import Leanpkg.Proc
-
-open Lean
-open System
-
-namespace Leanpkg.Build
-
-def buildPath : FilePath := "build"
-def tempBuildPath := buildPath / "temp"
-
-structure Config where
-  pkg      : Name
-  leanArgs : List String
-  leanPath : String
-  -- things like `leanpkg.toml` and olean roots of dependencies that should also trigger rebuilds
-  moreDeps : List FilePath
-
-structure Context extends Config where
-  parents       : List Name := []
-  moreDepsMTime : IO.FS.SystemTime
-
-structure Result where
-  maxMTime : IO.FS.SystemTime
-  task     : Task (Except IO.Error Unit)
-  deriving Inhabited
-
-structure State where
-  modTasks : NameMap Result := ∅
-
-abbrev BuildM := ReaderT Context <| StateT State IO
-
-partial def buildModule (mod : Name) : BuildM Result := do
-  let ctx ← read
-  if ctx.parents.contains mod then
-    -- cyclic import
-    let cycle := mod :: (ctx.parents.partition (· != mod)).1 ++ [mod]
-    let cycle := cycle.map (s!"  {·}")
-    throw <| IO.userError s!"import cycle detected:\n{"\n".intercalate cycle}"
-
-  if let some r := (← get).modTasks.find? mod then
-    -- already visited
-    return r
-
-  let leanFile := modToFilePath "." mod "lean"
-  let leanMData ← leanFile.metadata
-
-  -- recursively build dependencies and calculate transitive `maxMTime`
-  let (imports, _, _) ← Elab.parseImports (← IO.FS.readFile leanFile) leanFile.toString
-  let localImports := imports.filter (·.module.getRoot == ctx.pkg)
-  let deps ← localImports.mapM fun i =>
-    withReader (fun ctx => { ctx with parents := mod :: ctx.parents }) <|
-      buildModule i.module
-  let depMTimes := deps.map (·.maxMTime)
-  let maxMTime := List.maximum? (leanMData.modified :: ctx.moreDepsMTime :: depMTimes) |>.get!
-
-  -- check whether we have an up-to-date .olean
-  let oleanFile := modToFilePath buildPath mod "olean"
-  try
-    if (← oleanFile.metadata).modified >= maxMTime then
-      let r := { maxMTime, task := Task.pure (Except.ok ()) }
-      modify fun st => { st with modTasks := st.modTasks.insert mod r }
-      return r
-  catch
-    | IO.Error.noFileOrDirectory .. => pure ()
-    | e                             => throw e
-
-  let task ← IO.mapTasks (tasks := deps.map (·.task)) fun rs => do
-    if let some e := rs.findSome? (fun | Except.error e => some e | Except.ok _ => none) then
-      -- propagate failure
-      throw e
-    try
-      let cFile := modToFilePath tempBuildPath mod "c"
-      IO.FS.createDirAll oleanFile.parent.get!
-      IO.FS.createDirAll cFile.parent.get!
-      execCmd {
-        cmd := (← IO.appDir) / "lean" |>.withExtension FilePath.exeExtension |>.toString
-        args := ctx.leanArgs.toArray ++ #["-o", oleanFile.toString, "-c", cFile.toString, leanFile.toString]
-        env := #[("LEAN_PATH", ctx.leanPath)]
-      }
-    catch e =>
-      -- print errors early
-      IO.eprintln e
-      throw e
-
-  let r := { maxMTime, task := task }
-  modify fun st => { st with modTasks := st.modTasks.insert mod r }
-  return r
-
-def buildModules (cfg : Config) (mods : List Name) : IO Unit := do
-  let moreDepsMTime := (← cfg.moreDeps.mapM (·.metadata)).map (·.modified) |>.maximum? |>.getD ⟨0, 0⟩
-  let rs ← mods.mapM buildModule |>.run { toConfig := cfg, moreDepsMTime } |>.run' {}
-  for r in rs do
-    if let Except.error _ ← IO.wait r.task then
-      -- actual error has already been printed above
-      throw <| IO.userError "Build failed."
-
-end Leanpkg.Build

stage0/src/Leanpkg/Git.lean

@@ -1,40 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich
--/
-import Leanpkg.LeanVersion
-
-open System
-
-namespace Leanpkg
-
-def upstreamGitBranch :=
-  "master"
-
-def gitdefaultRevision : Option String → String
-  | none => upstreamGitBranch
-  | some branch => branch
-
-def gitParseRevision (gitRepo : FilePath) (rev : String) : IO String := do
-  let rev ← IO.Process.run {cmd := "git", args := #["rev-parse", "-q", "--verify", rev], cwd := gitRepo}
-  pure rev.trim -- remove newline at end
-
-def gitHeadRevision (gitRepo : FilePath) : IO String :=
-  gitParseRevision gitRepo "HEAD"
-
-def gitParseOriginRevision (gitRepo : FilePath) (rev : String) : IO String :=
-  (gitParseRevision gitRepo $ "origin/" ++ rev) <|> gitParseRevision gitRepo rev
-    <|> throw (IO.userError s!"cannot find revision {rev} in repository {gitRepo}")
-
-def gitLatestOriginRevision (gitRepo : FilePath) (branch : Option String) : IO String := do
-  discard <| IO.Process.run {cmd := "git", args := #["fetch"], cwd := gitRepo}
-  gitParseOriginRevision gitRepo (gitdefaultRevision branch)
-
-def gitRevisionExists (gitRepo : FilePath) (rev : String) : IO Bool := do
-  try
-    discard <| gitParseRevision gitRepo (rev ++ "^{commit}")
-    pure true
-  catch _ => pure false
-
-end Leanpkg

stage0/src/Leanpkg/LeanVersion.lean

@@ -1,29 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich
--/
-namespace Leanpkg
-
-def leanVersionStringCore :=
-  s!"{Lean.version.major}.{Lean.version.minor}.{Lean.version.patch}"
-
-def origin := "leanprover/lean4"
-
-def leanVersionString :=
-  if Lean.version.isRelease then
-      s!"{origin}:{leanVersionStringCore}"
-  else if Lean.version.specialDesc ≠ "" then
-      s!"{origin}:{Lean.version.specialDesc}"
-  else
-      s!"{origin}:master"
-
-def uiLeanVersionString :=
-if Lean.version.isRelease then
-    leanVersionStringCore
-else if Lean.version.specialDesc ≠ "" then
-    Lean.version.specialDesc
-else
-    s!"master ({leanVersionStringCore})"
-
-end Leanpkg

stage0/src/Leanpkg/Manifest.lean

@@ -1,87 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich
--/
-import Leanpkg.Toml
-import Leanpkg.LeanVersion
-
-open System
-
-namespace Leanpkg
-
-inductive Source where
-  | path (dir : System.FilePath) : Source
-  | git (url rev : String) (branch : Option String) : Source
-
-namespace Source
-
-def fromToml (v : Toml.Value) : OptionM Source :=
-  (do let Toml.Value.str dir ← v.lookup "path" | none
-      pure <| path ⟨dir⟩) <|>
-  (do let Toml.Value.str url ← v.lookup "git" | none
-      let Toml.Value.str rev ← v.lookup "rev" | none
-      match v.lookup "branch" with
-      | none                         => pure <| git url rev none
-      | some (Toml.Value.str branch) => pure <| git url rev (some branch)
-      | _ => none)
-
-def toToml : Source → Toml.Value
-  | path dir => Toml.Value.table [("path", Toml.Value.str dir.toString)]
-  | git url rev none =>
-    Toml.Value.table [("git", Toml.Value.str url), ("rev", Toml.Value.str rev)]
-  | git url rev (some branch) =>
-    Toml.Value.table [("git", Toml.Value.str url), ("branch", Toml.Value.str branch), ("rev", Toml.Value.str rev)]
-
-end Source
-
-structure Dependency where
-  name : String
-  src : Source
-
-structure Manifest where
-  name : String
-  version : String
-  leanVersion : String := leanVersionString
-  timeout : Option Nat := none
-  path : Option FilePath := none
-  dependencies : List Dependency := []
-
-namespace Manifest
-
-def effectivePath (m : Manifest) : FilePath :=
-  m.path.getD ⟨"."⟩
-
-def fromToml (t : Toml.Value) : Option Manifest := OptionM.run do
-  let pkg ← t.lookup "package"
-  let Toml.Value.str n ← pkg.lookup "name" | none
-  let Toml.Value.str ver ← pkg.lookup "version" | none
-  let leanVer ← match pkg.lookup "lean_version" with
-    | some (Toml.Value.str leanVer) => some leanVer
-    | none => some leanVersionString
-    | _ => none
-  let tm ← match pkg.lookup "timeout" with
-    | some (Toml.Value.nat timeout) => some (some timeout)
-    | none => some none
-    | _ => none
-  let path ← match pkg.lookup "path" with
-    | some (Toml.Value.str path) => some (some ⟨path⟩)
-    | none => some none
-    | _ => none
-  let Toml.Value.table deps ← t.lookup "dependencies" <|> some (Toml.Value.table []) | none
-  let deps ← deps.mapM fun ⟨n, src⟩ => return Dependency.mk n (← Source.fromToml src)
-  return { name := n, version := ver, leanVersion := leanVer,
-           path := path, dependencies := deps, timeout := tm }
-
-def fromFile (fn : System.FilePath) : IO Manifest := do
-  let cnts ← IO.FS.readFile fn
-  let toml ← Toml.parse cnts
-  let some manifest ← pure (fromToml toml)
-    | throw <| IO.userError s!"cannot read manifest from {fn}"
-  return manifest
-
-end Manifest
-
-def leanpkgTomlFn : System.FilePath := ⟨"leanpkg.toml"⟩
-
-end Leanpkg

stage0/src/Leanpkg/Proc.lean

@@ -1,20 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich
--/
-namespace Leanpkg
-
-def execCmd (args : IO.Process.SpawnArgs) : IO Unit := do
-  let envstr := String.join <| args.env.toList.map fun (k, v) => s!"{k}={v.getD ""} "
-  let cmdstr := " ".intercalate (args.cmd :: args.args.toList)
-  IO.eprintln <| "> " ++ envstr ++
-    match args.cwd with
-    | some cwd => s!"{cmdstr}    # in directory {cwd}"
-    | none     => cmdstr
-  let child ← IO.Process.spawn args
-  let exitCode ← child.wait
-  if exitCode != 0 then
-    throw <| IO.userError <| s!"external command exited with status {exitCode}"
-
-end Leanpkg

stage0/src/Leanpkg/Resolve.lean

@@ -1,84 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich
--/
-import Leanpkg.Manifest
-import Leanpkg.Proc
-import Leanpkg.Git
-
-open System
-
-namespace Leanpkg
-
-def Assignment := List (String × FilePath)
-
-namespace Assignment
-def empty : Assignment := []
-
-def contains (a : Assignment) (s : String) : Bool :=
-  (a.lookup s).isSome
-
-def insert (a : Assignment) (k : String) (v : FilePath) : Assignment :=
-  if a.contains k then a else (k, v) :: a
-
-def fold {α} (i : α) (f : α → String → FilePath → α) : Assignment → α :=
-  List.foldl (fun a ⟨k, v⟩ => f a k v) i
-
-end Assignment
-
-abbrev Solver := StateT Assignment IO
-
-def notYetAssigned (d : String) : Solver Bool :=
-  return ! (← get).contains d
-
-def resolvedPath (d : String) : Solver FilePath := do
-  let some path ← pure ((← get).lookup d) | unreachable!
-  return path
-
-def materialize (relpath : FilePath) (dep : Dependency) : Solver Unit :=
-  match dep.src with
-  | Source.path dir => do
-    let depdir := dir / relpath
-    IO.eprintln s!"{dep.name}: using local path {depdir}"
-    modify (·.insert dep.name depdir)
-  | Source.git url rev branch => do
-    let depdir := FilePath.mk "build" / "deps" / dep.name
-    if ← depdir.isDir then
-      IO.eprint s!"{dep.name}: trying to update {depdir} to revision {rev}"
-      IO.eprintln (match branch with | none => "" | some branch => "@" ++ branch)
-      let hash ← gitParseOriginRevision depdir rev
-      let revEx ← gitRevisionExists depdir hash
-      unless revEx do
-        execCmd {cmd := "git", args := #["fetch"], cwd := depdir}
-    else
-      IO.eprintln s!"{dep.name}: cloning {url} to {depdir}"
-      execCmd {cmd := "git", args := #["clone", url, depdir.toString]}
-    let hash ← gitParseOriginRevision depdir rev
-    execCmd {cmd := "git", args := #["checkout", "--detach", hash], cwd := depdir}
-    modify (·.insert dep.name depdir)
-
-def solveDepsCore (relPath : FilePath) (d : Manifest) : (maxDepth : Nat) → Solver Unit
-  | 0 => throw <| IO.userError "maximum dependency resolution depth reached"
-  | maxDepth + 1 => do
-    let deps ← d.dependencies.filterM (notYetAssigned ·.name)
-    deps.forM (materialize relPath)
-    for dep in deps do
-      let p ← resolvedPath dep.name
-      let d' ← Manifest.fromFile $ p / "leanpkg.toml"
-      unless d'.name = dep.name do
-        throw <| IO.userError s!"{d.name} (in {relPath}) depends on {d'.name}, but resolved dependency has name {dep.name} (in {p})"
-      solveDepsCore p d' maxDepth
-
-def solveDeps (d : Manifest) : IO Assignment := do
-  let (_, assg) ← (solveDepsCore ⟨"."⟩ d 1024).run <| Assignment.empty.insert d.name ⟨"."⟩
-  return assg
-
-def constructPathCore (depname : String) (dirname : FilePath) : IO FilePath := do
-  let path := Manifest.effectivePath (← Manifest.fromFile <| dirname / leanpkgTomlFn)
-  return dirname / path
-
-def constructPath (assg : Assignment) : IO (List FilePath) := do
-  assg.reverse.mapM fun ⟨depname, dirname⟩ => constructPathCore depname dirname
-
-end Leanpkg

stage0/src/Leanpkg/Toml.lean

@@ -1,72 +0,0 @@
-/-
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Sebastian Ullrich
--/
-import Lean.Parser
-
-namespace Toml
-
-inductive Value : Type where
-  | str : String → Value
-  | nat : Nat → Value
-  | bool : Bool → Value
-  | table : List (String × Value) → Value
-  deriving Inhabited
-
-def Value.lookup : Value → String → Option Value
-  | Value.table cs, k => cs.lookup k
-  | _, _ => none
-
--- TODO: custom whitespace and other inaccuracies
-declare_syntax_cat val
-syntax "True" : val
-syntax "False" : val
-syntax str : val
-syntax num : val
-syntax bareKey := ident  -- TODO
-syntax key := bareKey <|> str
-declare_syntax_cat keyCat @[keyCatParser] def key' := key  -- HACK: for the antiquotation
-syntax keyVal := key " = " val
-syntax table := "[" key "]" keyVal*
-syntax inlineTable := "{" keyVal,* "}"
-syntax inlineTable : val
-syntax file := table*
-declare_syntax_cat fileCat @[fileCatParser] def file' := file  -- HACK: for the antiquotation
-
-open Lean
-
-partial def ofSyntax : Syntax → Value
-  | `(val|True) => Value.bool true
-  | `(val|False) => Value.bool false
-  | `(val|$s:strLit) => Value.str <| s.isStrLit?.get!
-  | `(val|$n:numLit) => Value.nat <| n.isNatLit?.get!
-  | `(val|{$[$keys:key = $values],*}) => toTable keys (values.map ofSyntax)
-  | `(fileCat|$[[$keys] $kvss*]*) => toTable keys <| kvss.map fun kvs => ofSyntax <| Lean.Unhygienic.run `(val|{$kvs,*})
-  | stx => unreachable!
-  where
-    toKey : Syntax → String
-      | `(keyCat|$key:ident)  => key.getId.toString
-      | `(keyCat|$key:strLit) => key.isStrLit?.get!
-      | _                     => unreachable!
-    toTable (keys : Array Syntax) (vals : Array Value) : Value :=
-      Value.table <| Array.toList <| keys.zipWith vals fun k v => (toKey k, v)
-
-open Lean.Parser
-
-def parse (input : String) : IO Value := do
-  -- HACKHACKHACK
-  let env ← importModules [{ module := `Leanpkg.Toml }] {}
-  let fileParser ← compileParserDescr (parserExtension.getState env).categories file { env := env, opts := {} }
-  let c := mkParserContext (mkInputContext input "") { env := env, options := {} }
-  let s := mkParserState input
-  let s := whitespace c s
-  let s := fileParser.fn c s
-  if s.hasError then
-    throw <| IO.userError (s.toErrorMsg c)
-  else if input.atEnd s.pos then
-    return ofSyntax s.stxStack.back
-  else
-    throw <| IO.userError ((s.mkError "end of input").toErrorMsg c)
-
-end Toml

stage0/src/shell/CMakeLists.txt

@@ -148,82 +148,8 @@ FOREACH(T ${LEANTESTS})
   endif()
 ENDFOREACH(T)
 
-add_test(NAME leanpkgtest
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/b"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           leanpkg build
-           # linking requires some manual steps
-           (cd ../a; leanpkg build lib)
-           leanpkg build bin LINK_OPTS=../a/build/lib/libA.a
-           ./build/bin/B")
-
-add_test(NAME leanpkgtest_cyclic
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/cyclic"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           leanpkg build 2>&1 | grep 'import cycle'")
-
-add_test(NAME leanpkgtest_user_ext
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_ext"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           find . -name '*.olean' -delete
-           leanmake | grep 'world, hello, test'")
-
-add_test(NAME leanpkgtest_user_attr
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_attr"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           find . -name '*.olean' -delete
-           leanmake")
-
-add_test(NAME leanpkgtest_user_deriving
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/deriving"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           find . -name '*.olean' -delete
-           leanmake")
-
-add_test(NAME leanpkgtest_user_opt
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_opt"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           find . -name '*.olean' -delete
-           leanmake")
-
-add_test(NAME leanpkgtest_prv
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/prv"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           find . -name '*.olean' -delete
-           leanmake 2>&1 | grep 'error: field.*private'")
-
-add_test(NAME leanpkgtest_user_attr_app
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/user_attr_app"
-         COMMAND bash -c "
-           set -eu
-           export ${TEST_VARS}
-           find . -name '*.olean' -delete
-           leanmake bin LINK_OPTS='${LEAN_DYN_EXE_LINKER_FLAGS}' && build/bin/UserAttr")
-
-add_test(NAME leanpkgtest_builtin_attr
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/leanpkg/builtin_attr"
-         COMMAND bash -c "
-           set -eu
-           export PATH=${LEAN_BIN}:$PATH
-           find . -name '*.olean' -delete
-           leanmake")
-
 # Create a lake test for each subdirectory of `lake/examples` which contains a `test.sh` file.
-# We skip the subdirectories `lean_packages` and `bootstrap` since `lake/examples/Makefile` do no consider them.
+# We skip the subdirectories `lean_packages` and `bootstrap` since `lake/examples/Makefile` does not consider them either.
 file(GLOB_RECURSE LEANLAKETESTS "${LEAN_SOURCE_DIR}/lake/examples/test.sh")
 FOREACH(T ${LEANLAKETESTS})
   if(NOT T MATCHES ".*lean_packages.*")

stage0/src/stdlib.make.in

@@ -24,7 +24,7 @@ ifeq "${STAGE}" "0"
   LEANMAKE_OPTS+=C_ONLY=1 C_OUT=../stdlib/
 endif
 
-.PHONY: Init Std Lean leanshared Leanpkg Lake lean
+.PHONY: Init Std Lean leanshared Lake lean
 
 # These can be phony since the inner Makefile will have the correct dependencies and avoid rebuilds
 Init:
@@ -46,9 +46,6 @@ ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: $
 
 leanshared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}
 
-Leanpkg:
-	+"${LEAN_BIN}/leanmake" bin PKG=Leanpkg BIN_NAME=leanpkg${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='-lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}'
-
 Lake:
 # must put lake in its own directory because of submodule, so must adjust relative paths...
 	+"${LEAN_BIN}/leanmake" -C lake bin PKG=Lake BIN_NAME=lake${CMAKE_EXECUTABLE_SUFFIX} $(LEANMAKE_OPTS) LINK_OPTS='-lleanshared ${CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE}' OUT="../${LIB}" LIB_OUT="../${LIB}/lean" OLEAN_OUT="../${LIB}/lean"

stage0/stdlib/Lean/Compiler/ExternAttr.c

@@ -83,6 +83,7 @@ static lean_object* l_Lean_getExternConstArityExport___closed__5;
 extern lean_object* l_Lean_numLitKind;
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Compiler_ExternAttr___hyg_397____lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_ExternAttrData_arity_x3f___default;
 LEAN_EXPORT lean_object* l_Lean_expandExternPatternAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_getExternConstArityExport___closed__3;
@@ -141,7 +142,6 @@ LEAN_EXPORT lean_object* l_Lean_addExtern___boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_getExternEntryFor(lean_object*, lean_object*);
 static lean_object* l_Lean_getExternConstArityExport___closed__6;
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Compiler_ExternAttr_0__Lean_syntaxToExternAttrData___spec__3(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
-uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Compiler_ExternAttr_0__Lean_syntaxToExternAttrData___spec__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_mul(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_throwError___at___private_Lean_Compiler_ExternAttr_0__Lean_getExternConstArity___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -674,7 +674,7 @@ else
 {
 lean_object* x_17; uint8_t x_18; 
 x_17 = lean_box(0);
-x_18 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1(x_14, x_17);
+x_18 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1(x_14, x_17);
 if (x_18 == 0)
 {
 lean_object* x_19; lean_object* x_20; 

stage0/stdlib/Lean/Elab/PreDefinition/Main.c

@@ -140,6 +140,7 @@ static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinit
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_addPreDefinitions___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1(lean_object*, lean_object*);
 static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__4;
 LEAN_EXPORT lean_object* l___private_Lean_Util_SCC_0__Lean_SCC_getDataOf___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__7(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_partitionPreDefs___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -248,7 +249,6 @@ lean_object* l_Lean_Elab_WF_TerminationBy_ensureAllUsed(lean_object*, lean_objec
 LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_addPreDefinitions___spec__4___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_addPreDefinitions___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_addPreDefinitions___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Term_Quotation_getAntiquotationIds___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Main_0__Lean_Elab_addAndCompilePartial___spec__2___lambda__2___closed__3;
 lean_object* lean_nat_mul(lean_object*, lean_object*);
@@ -2597,7 +2597,7 @@ lean_inc(x_13);
 x_14 = lean_ctor_get(x_11, 0);
 lean_inc(x_14);
 lean_dec(x_11);
-x_15 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1(x_13, x_14);
+x_15 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1(x_13, x_14);
 lean_dec(x_14);
 lean_dec(x_13);
 if (x_15 == 0)
@@ -2630,7 +2630,7 @@ lean_inc(x_20);
 x_21 = lean_ctor_get(x_18, 0);
 lean_inc(x_21);
 lean_dec(x_18);
-x_22 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1(x_20, x_21);
+x_22 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1(x_20, x_21);
 lean_dec(x_21);
 lean_dec(x_20);
 if (x_22 == 0)

stage0/stdlib/Lean/Elab/PreDefinition/Structural/SmartUnfolding.c

@@ -37,7 +37,6 @@ lean_object* lean_expr_instantiate1(lean_object*, lean_object*);
 lean_object* l_Array_toSubarray___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
-lean_object* l_Lean_Meta_markSmartUnfoldigMatchAlt(lean_object*);
 lean_object* l_Lean_Meta_smartUnfoldingMatch_x3f(lean_object*);
 uint8_t lean_usize_dec_lt(size_t, size_t);
 extern lean_object* l_Lean_levelZero;
@@ -85,6 +84,7 @@ lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Structural_addSmartUnfoldingDefAux_visit___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_Match_MatcherInfo_arity(lean_object*);
 lean_object* lean_mk_array(lean_object*, lean_object*);
+lean_object* l_Lean_Meta_markSmartUnfoldingMatchAlt(lean_object*);
 static lean_object* l_Lean_Meta_matchMatcherApp_x3f___at_Lean_Elab_Structural_addSmartUnfoldingDefAux_visit___spec__1___closed__1;
 lean_object* l_Lean_Meta_getMatcherInfo_x3f___at_Lean_Meta_reduceMatcher_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Structural_addSmartUnfoldingDef(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -995,7 +995,7 @@ lean_inc(x_23);
 x_24 = lean_ctor_get(x_22, 1);
 lean_inc(x_24);
 lean_dec(x_22);
-x_25 = l_Lean_Meta_markSmartUnfoldigMatchAlt(x_23);
+x_25 = l_Lean_Meta_markSmartUnfoldingMatchAlt(x_23);
 x_26 = lean_unsigned_to_nat(0u);
 x_27 = l_Array_toSubarray___rarg(x_4, x_26, x_5);
 x_28 = l_Array_ofSubarray___rarg(x_27);

stage0/stdlib/Lean/Elab/Quotation.c

@@ -390,6 +390,7 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
 static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_floatOutAntiquotTerms___lambda__2___closed__4;
 static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__8___closed__2;
 static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3813____closed__5;
+uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1(lean_object*, lean_object*);
 static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_floatOutAntiquotTerms___lambda__2___closed__17;
 LEAN_EXPORT lean_object* l_Lean_Elab_Term_Quotation___aux__Lean__Elab__Quotation______macroRules__Lean__Elab__Term__Quotation__commandElab__stx__quot______1(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Term_Quotation_match__syntax_expand___spec__3___boxed(lean_object*, lean_object*, lean_object*);
@@ -867,7 +868,6 @@ static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean
 static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__14;
 static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_getHeadInfo___lambda__14___closed__19;
 static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___lambda__1___closed__1;
-uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1(lean_object*, lean_object*);
 static lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_floatOutAntiquotTerms___lambda__2___closed__3;
 static lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabQuot____x40_Lean_Elab_Quotation___hyg_3813__declRange___closed__1;
 lean_object* l_Lean_throwErrorAt___at_Lean_Elab_Term_Quotation_getAntiquotationIds___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -19044,7 +19044,7 @@ lean_object* x_10; lean_object* x_11; uint8_t x_12;
 x_10 = lean_array_get_size(x_2);
 x_11 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_11, 0, x_10);
-x_12 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1(x_7, x_11);
+x_12 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1(x_7, x_11);
 lean_dec(x_11);
 lean_dec(x_7);
 if (x_12 == 0)

stage0/stdlib/Lean/Elab/Tactic/Match.c

@@ -48,6 +48,7 @@ lean_object* l_Lean_Elab_Tactic_evalTacticAux(lean_object*, lean_object*, lean_o
 LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_AuxMatchTermState_cases___default;
 size_t lean_usize_sub(size_t, size_t);
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalEraseAuxDiscrs___closed__5;
+static lean_object* l_Lean_Elab_Tactic_evalMatch___closed__4;
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalEraseAuxDiscrs___closed__15;
 static lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTermAux___spec__2___closed__23;
@@ -178,6 +179,7 @@ lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Tactic_evalMatch___spec__1___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux___at_Lean_Elab_Tactic_evalEraseAuxDiscrs___spec__3(lean_object*, size_t, size_t, lean_object*);
 lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Elab_Tactic_evalMatch___closed__5;
 static lean_object* l_Lean_Elab_Tactic_evalEraseAuxDiscrs___rarg___closed__1;
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalMatch___closed__4;
 static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalEraseAuxDiscrs___closed__4;
@@ -212,6 +214,7 @@ static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalMatch_declRange___closed
 uint8_t lean_string_dec_eq(lean_object*, lean_object*);
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 static lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTermAux___spec__2___closed__36;
+static lean_object* l_Lean_Elab_Tactic_evalMatch___closed__3;
 LEAN_EXPORT lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_evalEraseAuxDiscrs___spec__5(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
 _start:
 {
@@ -3537,6 +3540,32 @@ x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
+static lean_object* _init_l_Lean_Elab_Tactic_evalMatch___closed__3() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("noImplicitLambda");
+return x_1;
+}
+}
+static lean_object* _init_l_Lean_Elab_Tactic_evalMatch___closed__4() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTermAux___spec__2___closed__2;
+x_2 = l_Lean_Elab_Tactic_evalMatch___closed__3;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+static lean_object* _init_l_Lean_Elab_Tactic_evalMatch___closed__5() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("no_implicit_lambda%");
+return x_1;
+}
+}
 LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalMatch(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
 _start:
 {
@@ -3573,7 +3602,7 @@ lean_inc(x_2);
 x_15 = l_Lean_Elab_liftMacroM___at_Lean_Elab_Tactic_evalMatch___spec__1(x_14, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_13);
 if (lean_obj_tag(x_15) == 0)
 {
-lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; 
+lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; 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; 
 x_16 = lean_ctor_get(x_15, 0);
 lean_inc(x_16);
 x_17 = lean_ctor_get(x_15, 1);
@@ -3600,37 +3629,49 @@ x_26 = lean_ctor_get(x_25, 1);
 lean_inc(x_26);
 lean_dec(x_25);
 x_27 = l_Lean_Elab_Tactic_evalMatch___closed__1;
+lean_inc(x_21);
 x_28 = lean_alloc_ctor(2, 2, 0);
 lean_ctor_set(x_28, 0, x_21);
 lean_ctor_set(x_28, 1, x_27);
-x_29 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTermAux___spec__2___closed__14;
-x_30 = lean_array_push(x_29, x_28);
-x_31 = lean_array_push(x_30, x_18);
-x_32 = lean_box(2);
-x_33 = l_Lean_Elab_Tactic_evalMatch___closed__2;
-x_34 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_34, 0, x_32);
-lean_ctor_set(x_34, 1, x_33);
-lean_ctor_set(x_34, 2, x_31);
-x_35 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTermAux___spec__2___closed__27;
-x_36 = lean_array_push(x_35, x_34);
-x_37 = l_Array_append___rarg(x_36, x_19);
-x_38 = l_Lean_nullKind;
-x_39 = lean_alloc_ctor(1, 3, 0);
-lean_ctor_set(x_39, 0, x_32);
-lean_ctor_set(x_39, 1, x_38);
-lean_ctor_set(x_39, 2, x_37);
-lean_inc(x_39);
+x_29 = l_Lean_Elab_Tactic_evalMatch___closed__5;
+x_30 = lean_alloc_ctor(2, 2, 0);
+lean_ctor_set(x_30, 0, x_21);
+lean_ctor_set(x_30, 1, x_29);
+x_31 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTermAux___spec__2___closed__14;
+x_32 = lean_array_push(x_31, x_30);
+x_33 = lean_array_push(x_32, x_18);
+x_34 = lean_box(2);
+x_35 = l_Lean_Elab_Tactic_evalMatch___closed__4;
+x_36 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_36, 0, x_34);
+lean_ctor_set(x_36, 1, x_35);
+lean_ctor_set(x_36, 2, x_33);
+x_37 = lean_array_push(x_31, x_28);
+x_38 = lean_array_push(x_37, x_36);
+x_39 = l_Lean_Elab_Tactic_evalMatch___closed__2;
+x_40 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_40, 0, x_34);
+lean_ctor_set(x_40, 1, x_39);
+lean_ctor_set(x_40, 2, x_38);
+x_41 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Tactic_Match_0__Lean_Elab_Tactic_mkAuxiliaryMatchTermAux___spec__2___closed__27;
+x_42 = lean_array_push(x_41, x_40);
+x_43 = l_Array_append___rarg(x_42, x_19);
+x_44 = l_Lean_nullKind;
+x_45 = lean_alloc_ctor(1, 3, 0);
+lean_ctor_set(x_45, 0, x_34);
+lean_ctor_set(x_45, 1, x_44);
+lean_ctor_set(x_45, 2, x_43);
+lean_inc(x_45);
 lean_inc(x_1);
-x_40 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalMatch___lambda__1), 11, 2);
-lean_closure_set(x_40, 0, x_1);
-lean_closure_set(x_40, 1, x_39);
-x_41 = l_Lean_Elab_withMacroExpansionInfo___at_Lean_Elab_Tactic_adaptExpander___spec__1(x_1, x_39, x_40, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_26);
-return x_41;
+x_46 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalMatch___lambda__1), 11, 2);
+lean_closure_set(x_46, 0, x_1);
+lean_closure_set(x_46, 1, x_45);
+x_47 = l_Lean_Elab_withMacroExpansionInfo___at_Lean_Elab_Tactic_adaptExpander___spec__1(x_1, x_45, x_46, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_26);
+return x_47;
 }
 else
 {
-uint8_t x_42; 
+uint8_t x_48; 
 lean_dec(x_9);
 lean_dec(x_8);
 lean_dec(x_7);
@@ -3640,29 +3681,29 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_42 = !lean_is_exclusive(x_15);
-if (x_42 == 0)
+x_48 = !lean_is_exclusive(x_15);
+if (x_48 == 0)
 {
 return x_15;
 }
 else
 {
-lean_object* x_43; lean_object* x_44; lean_object* x_45; 
-x_43 = lean_ctor_get(x_15, 0);
-x_44 = lean_ctor_get(x_15, 1);
-lean_inc(x_44);
-lean_inc(x_43);
+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_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;
+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;
 }
 }
 }
 else
 {
-uint8_t x_46; 
+uint8_t x_52; 
 lean_dec(x_9);
 lean_dec(x_8);
 lean_dec(x_7);
@@ -3672,23 +3713,23 @@ lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_46 = !lean_is_exclusive(x_11);
-if (x_46 == 0)
+x_52 = !lean_is_exclusive(x_11);
+if (x_52 == 0)
 {
 return x_11;
 }
 else
 {
-lean_object* x_47; lean_object* x_48; lean_object* x_49; 
-x_47 = lean_ctor_get(x_11, 0);
-x_48 = lean_ctor_get(x_11, 1);
-lean_inc(x_48);
-lean_inc(x_47);
+lean_object* x_53; lean_object* x_54; lean_object* x_55; 
+x_53 = lean_ctor_get(x_11, 0);
+x_54 = lean_ctor_get(x_11, 1);
+lean_inc(x_54);
+lean_inc(x_53);
 lean_dec(x_11);
-x_49 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_49, 0, x_47);
-lean_ctor_set(x_49, 1, x_48);
-return x_49;
+x_55 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_55, 0, x_53);
+lean_ctor_set(x_55, 1, x_54);
+return x_55;
 }
 }
 }
@@ -4131,6 +4172,12 @@ l_Lean_Elab_Tactic_evalMatch___closed__1 = _init_l_Lean_Elab_Tactic_evalMatch___
 lean_mark_persistent(l_Lean_Elab_Tactic_evalMatch___closed__1);
 l_Lean_Elab_Tactic_evalMatch___closed__2 = _init_l_Lean_Elab_Tactic_evalMatch___closed__2();
 lean_mark_persistent(l_Lean_Elab_Tactic_evalMatch___closed__2);
+l_Lean_Elab_Tactic_evalMatch___closed__3 = _init_l_Lean_Elab_Tactic_evalMatch___closed__3();
+lean_mark_persistent(l_Lean_Elab_Tactic_evalMatch___closed__3);
+l_Lean_Elab_Tactic_evalMatch___closed__4 = _init_l_Lean_Elab_Tactic_evalMatch___closed__4();
+lean_mark_persistent(l_Lean_Elab_Tactic_evalMatch___closed__4);
+l_Lean_Elab_Tactic_evalMatch___closed__5 = _init_l_Lean_Elab_Tactic_evalMatch___closed__5();
+lean_mark_persistent(l_Lean_Elab_Tactic_evalMatch___closed__5);
 l___regBuiltin_Lean_Elab_Tactic_evalMatch___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalMatch___closed__1();
 lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalMatch___closed__1);
 l___regBuiltin_Lean_Elab_Tactic_evalMatch___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_evalMatch___closed__2();

stage0/stdlib/Lean/Meta/Basic.c

@@ -40,7 +40,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_Cache_synthInstance___default;
 LEAN_EXPORT lean_object* l_Lean_Meta_mkFreshLevelMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
 lean_object* l_Lean_Level_collectMVars(lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1___boxed(lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_Lean_Meta_Config_transparency___default;
 LEAN_EXPORT lean_object* l_Lean_Meta_withLetDecl(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_withLocalDecl___at_Lean_Meta_withLocalDecls_loop___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
@@ -102,7 +101,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_savingCache(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_mkConstWithFreshMVarLevels(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Name_quickLt(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_mkFreshExprMVarAt___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_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__4;
 static lean_object* l_Lean_addTrace___at_Lean_Meta_processPostponed_loop___spec__1___closed__1;
 static lean_object* l_Lean_Meta_mkFunUnit___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Meta_withMCtx___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -127,6 +125,7 @@ LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_Meta_sortFVarIds___spec__1
 lean_object* l_Lean_Core_restore(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_instOrElseMetaM___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Meta_occursCheck(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__3;
 static lean_object* l_Lean_MetavarContext_instantiateExprMVars___at_Lean_Meta_instantiateMVars___spec__1___closed__1;
 lean_object* l_Lean_MetavarContext_getExprAssignment_x3f(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaFVarIds___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -161,6 +160,7 @@ uint8_t l_Lean_Level_hasMVar(lean_object*);
 lean_object* l_Std_PersistentArray_append___rarg(lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_instInhabitedState___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Meta_withNewBinderInfos___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__4;
 LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescope(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_dependsOn(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
@@ -210,6 +210,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_hasAssignableMVar___boxed(lean_object*, lea
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_exposeRelevantUniverses___lambda__1(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_getLevelMVarDepth___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
+LEAN_EXPORT uint8_t l_Lean_Meta_ParamInfo_isProp___default;
 LEAN_EXPORT lean_object* l_Lean_Meta_setMVarType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_isClass_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_withLCtx___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -262,7 +263,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_withMVarContext(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_modifyInferTypeCache(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_getPostponed___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Array_qsort_sort___at_Lean_Meta_sortFVarIds___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_4_(lean_object*);
 LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___spec__11___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_getPostponed___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -296,11 +297,13 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkLeveErrorMes
 static lean_object* l_Lean_Meta_State_mctx___default___closed__3;
 LEAN_EXPORT lean_object* l_Lean_Meta_withLocalDeclsD(lean_object*);
 static lean_object* l_Lean_Meta_localDeclDependsOnPred___closed__1;
+LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____boxed(lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_Context_lctx___default___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Meta_instantiateForall(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_instAlternativeMetaM___closed__1;
 LEAN_EXPORT lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_LocalContext_setBinderInfo(lean_object*, lean_object*, uint8_t);
+LEAN_EXPORT uint8_t l_Lean_Meta_ParamInfo_isDecInst___default;
 static lean_object* l_Lean_Meta_throwUnknownFVar___rarg___closed__1;
 LEAN_EXPORT lean_object* l_Lean_Meta_isInductivePredicate(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_getConfig___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -349,7 +352,6 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContex
 LEAN_EXPORT lean_object* l_Lean_Meta_map2MetaM(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_exposeRelevantUniverses(lean_object*, lean_object*);
 lean_object* l_Lean_Expr_setPPUniverses(lean_object*, uint8_t);
-static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__3;
 lean_object* l_Lean_MessageData_toString(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_Context_synthPendingDepth___default;
 LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Meta_mkFreshExprMVarAt___spec__2___rarg(lean_object*, lean_object*);
@@ -378,6 +380,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_withLocalDecls_loop___rarg___lambda__1___bo
 LEAN_EXPORT lean_object* l_Lean_Meta_resetZetaFVarIds___boxed(lean_object*);
 LEAN_EXPORT lean_object* l_Std_PersistentArray_forIn___at___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l___private_Lean_Meta_Basic_0__Lean_Meta_fvarsSizeLtMaxFVars(lean_object*, lean_object*);
+LEAN_EXPORT uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1(lean_object*, lean_object*);
 lean_object* lean_array_swap(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_instMetaEvalMetaM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
 LEAN_EXPORT uint8_t l___private_Lean_Meta_Basic_0__Lean_Meta_mkLeveErrorMessageCore___lambda__1(lean_object*, lean_object*);
@@ -574,7 +577,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_getLevelMVarDepth(lean_object*, lean_object
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_instantiateLambdaAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_forallMetaTelescopeReducing___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_setEnv___at_Lean_Meta_setInlineAttribute___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT uint8_t l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321_(lean_object*, lean_object*);
+LEAN_EXPORT uint8_t l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341_(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_PersistentArray_forInAux___at___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___spec__3(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_mkFVar(lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withNewLocalInstancesImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -758,7 +761,6 @@ LEAN_EXPORT lean_object* l_Lean_Meta_assignLevelMVar___boxed(lean_object*, lean_
 LEAN_EXPORT lean_object* l_Lean_Meta_withReducible___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_isExprMVarAssigned(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_mkFreshExprMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-LEAN_EXPORT uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1(lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_processPostponed_loop___lambda__2___closed__2;
 uint8_t lean_get_reducibility_status(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_fvarsSizeLtMaxFVars___boxed(lean_object*, lean_object*);
@@ -779,7 +781,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_throwIsDefEqStuck___boxed(lean_object*, lea
 static lean_object* l_Lean_Meta_processPostponed_loop___closed__4;
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_approxDefEqImp(lean_object*);
 lean_object* l_Lean_mkForall(lean_object*, uint8_t, lean_object*, lean_object*);
-LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Meta_Basic___hyg_13187_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Meta_Basic___hyg_13207_(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_instMonadMCtxMetaM___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_addMessageContextFull___at_Lean_Meta_instAddMessageContextMetaM___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_resettingSynthInstanceCacheWhen(lean_object*);
@@ -796,6 +798,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_mkLambdaFVars___boxed(lean_object*, lean_ob
 lean_object* lean_level_update_succ(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_withMVarContext___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_infer_type(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__1;
 LEAN_EXPORT lean_object* l_Lean_Meta_instantiateMVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_isExprDefEq(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -877,6 +880,7 @@ LEAN_EXPORT lean_object* l_List_mapM___at_Lean_Meta_instantiateMVars___spec__3__
 LEAN_EXPORT lean_object* l_Lean_Meta_setInlineAttribute(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_withTrackingZeta(lean_object*);
 static lean_object* l_Lean_Meta_isLevelDefEq___closed__2;
+static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__2;
 LEAN_EXPORT lean_object* l_Lean_Meta_getLocalDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_Context_localInstances___default;
 LEAN_EXPORT lean_object* l___private_Lean_Util_Trace_0__Lean_getResetTraces___at___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___spec__7(lean_object*, lean_object*, lean_object*);
@@ -906,7 +910,6 @@ LEAN_EXPORT lean_object* l_Std_PersistentArray_forInAux___at___private_Lean_Meta
 LEAN_EXPORT lean_object* l_Lean_mkFreshMVarId___at_Lean_Meta_mkFreshExprMVarAt___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_mkFreshFVarId___at___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux_process___spec__1(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLetDeclImp(lean_object*);
-LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____boxed(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLetDeclImp___rarg(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_withAtLeastTransparency___rarg___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_Meta_Context_defEqCtx_x3f___default;
@@ -942,6 +945,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_withoutProofIrrelevance___rarg(lean_object*
 LEAN_EXPORT lean_object* l_Lean_Meta_orElse(lean_object*);
 LEAN_EXPORT uint8_t l_Array_qsort_sort___at_Lean_Meta_sortFVarIds___spec__1___lambda__1(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_forallBoundedTelescope___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1___boxed(lean_object*, lean_object*);
 static lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___closed__5;
 lean_object* l_Lean_mkConst(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_getConfig(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -964,7 +968,6 @@ LEAN_EXPORT lean_object* l_Lean_mkFreshFVarId___at___private_Lean_Meta_Basic_0__
 size_t lean_usize_of_nat(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_abstract___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_resettingSynthInstanceCache___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__1;
 LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescopeReducing___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_shouldReduceAll___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -987,7 +990,6 @@ LEAN_EXPORT uint8_t l_Lean_Meta_ParamInfo_isStrictImplicit(lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_instMonadMetaM___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassImp_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__2;
 LEAN_EXPORT lean_object* l_Lean_Meta_getFVarLocalDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_lambdaTelescopeImp_process___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_throwUnknownFVar___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -1177,6 +1179,22 @@ x_1 = l_Lean_Meta_ParamInfo_backDeps___default___closed__1;
 return x_1;
 }
 }
+static uint8_t _init_l_Lean_Meta_ParamInfo_isProp___default() {
+_start:
+{
+uint8_t x_1; 
+x_1 = 0;
+return x_1;
+}
+}
+static uint8_t _init_l_Lean_Meta_ParamInfo_isDecInst___default() {
+_start:
+{
+uint8_t x_1; 
+x_1 = 0;
+return x_1;
+}
+}
 static lean_object* _init_l_Lean_Meta_instInhabitedParamInfo___closed__1() {
 _start:
 {
@@ -1184,10 +1202,12 @@ uint8_t x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4;
 x_1 = 0;
 x_2 = 0;
 x_3 = l_Lean_Meta_ParamInfo_backDeps___default___closed__1;
-x_4 = lean_alloc_ctor(0, 1, 2);
+x_4 = lean_alloc_ctor(0, 1, 4);
 lean_ctor_set(x_4, 0, x_3);
 lean_ctor_set_uint8(x_4, sizeof(void*)*1, x_1);
 lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 1, x_2);
+lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 2, x_2);
+lean_ctor_set_uint8(x_4, sizeof(void*)*1 + 3, x_2);
 return x_4;
 }
 }
@@ -1350,7 +1370,7 @@ x_1 = l_Lean_Meta_instInhabitedInfoCacheKey___closed__3;
 return x_1;
 }
 }
-LEAN_EXPORT uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1(lean_object* x_1, lean_object* x_2) {
+LEAN_EXPORT uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 if (lean_obj_tag(x_1) == 0)
@@ -1387,7 +1407,7 @@ return x_8;
 }
 }
 }
-LEAN_EXPORT uint8_t l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321_(lean_object* x_1, lean_object* x_2) {
+LEAN_EXPORT uint8_t l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341_(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 uint8_t x_3; lean_object* x_4; lean_object* x_5; uint8_t x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9; 
@@ -1417,28 +1437,28 @@ return x_12;
 else
 {
 uint8_t x_13; 
-x_13 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1(x_5, x_8);
+x_13 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1(x_5, x_8);
 return x_13;
 }
 }
 }
 }
-LEAN_EXPORT lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1___boxed(lean_object* x_1, lean_object* x_2) {
+LEAN_EXPORT lean_object* l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 uint8_t x_3; lean_object* x_4; 
-x_3 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1(x_1, x_2);
+x_3 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1(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___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____boxed(lean_object* x_1, lean_object* x_2) {
+LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {
 uint8_t x_3; lean_object* x_4; 
-x_3 = l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321_(x_1, x_2);
+x_3 = l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341_(x_1, x_2);
 lean_dec(x_2);
 lean_dec(x_1);
 x_4 = lean_box(x_3);
@@ -1449,7 +1469,7 @@ static lean_object* _init_l_Lean_Meta_instBEqInfoCacheKey___closed__1() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____boxed), 2, 0);
+x_1 = lean_alloc_closure((void*)(l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____boxed), 2, 0);
 return x_1;
 }
 }
@@ -4056,7 +4076,7 @@ lean_dec(x_2);
 return x_6;
 }
 }
-static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__1() {
+static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -4064,17 +4084,17 @@ x_1 = lean_mk_string("Meta");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__2() {
+static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__1;
+x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__3() {
+static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -4082,21 +4102,21 @@ x_1 = lean_mk_string("debug");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__4() {
+static lean_object* _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__2;
-x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__3;
+x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__2;
+x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__3;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
-x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__2;
+x_2 = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__2;
 x_3 = l_Lean_registerTraceClass(x_2, x_1);
 if (lean_obj_tag(x_3) == 0)
 {
@@ -4104,7 +4124,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6;
 x_4 = lean_ctor_get(x_3, 1);
 lean_inc(x_4);
 lean_dec(x_3);
-x_5 = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__4;
+x_5 = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__4;
 x_6 = l_Lean_registerTraceClass(x_5, x_4);
 return x_6;
 }
@@ -31957,7 +31977,7 @@ static lean_object* _init_l___private_Lean_Meta_Basic_0__Lean_Meta_processPostpo
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__2;
+x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__2;
 x_2 = l___private_Lean_Meta_Basic_0__Lean_Meta_processPostponedStep___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@@ -38295,7 +38315,7 @@ static lean_object* _init_l_Lean_Meta_isExprDefEq___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__2;
+x_1 = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__2;
 x_2 = l_Lean_Meta_isExprDefEq___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
@@ -40562,7 +40582,7 @@ return x_72;
 }
 }
 }
-LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Meta_Basic___hyg_13187_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_initFn____x40_Lean_Meta_Basic___hyg_13207_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
@@ -40669,6 +40689,8 @@ l_Lean_Meta_ParamInfo_backDeps___default___closed__1 = _init_l_Lean_Meta_ParamIn
 lean_mark_persistent(l_Lean_Meta_ParamInfo_backDeps___default___closed__1);
 l_Lean_Meta_ParamInfo_backDeps___default = _init_l_Lean_Meta_ParamInfo_backDeps___default();
 lean_mark_persistent(l_Lean_Meta_ParamInfo_backDeps___default);
+l_Lean_Meta_ParamInfo_isProp___default = _init_l_Lean_Meta_ParamInfo_isProp___default();
+l_Lean_Meta_ParamInfo_isDecInst___default = _init_l_Lean_Meta_ParamInfo_isDecInst___default();
 l_Lean_Meta_instInhabitedParamInfo___closed__1 = _init_l_Lean_Meta_instInhabitedParamInfo___closed__1();
 lean_mark_persistent(l_Lean_Meta_instInhabitedParamInfo___closed__1);
 l_Lean_Meta_instInhabitedParamInfo = _init_l_Lean_Meta_instInhabitedParamInfo();
@@ -40860,15 +40882,15 @@ l_Lean_Meta_throwIsDefEqStuck___rarg___closed__1 = _init_l_Lean_Meta_throwIsDefE
 lean_mark_persistent(l_Lean_Meta_throwIsDefEqStuck___rarg___closed__1);
 l_Lean_Meta_throwIsDefEqStuck___rarg___closed__2 = _init_l_Lean_Meta_throwIsDefEqStuck___rarg___closed__2();
 lean_mark_persistent(l_Lean_Meta_throwIsDefEqStuck___rarg___closed__2);
-l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__1();
-lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__1);
-l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__2();
-lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__2);
-l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__3();
-lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__3);
-l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__4();
-lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329____closed__4);
-res = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1329_(lean_io_mk_world());
+l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__1 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__1();
+lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__1);
+l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__2 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__2();
+lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__2);
+l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__3 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__3();
+lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__3);
+l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__4 = _init_l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__4();
+lean_mark_persistent(l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349____closed__4);
+res = l_Lean_Meta_initFn____x40_Lean_Meta_Basic___hyg_1349_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 l_Lean_throwMaxRecDepthAt___at_Lean_Meta_withIncRecDepth___spec__1___rarg___closed__1 = _init_l_Lean_throwMaxRecDepthAt___at_Lean_Meta_withIncRecDepth___spec__1___rarg___closed__1();
@@ -41037,7 +41059,7 @@ l_Lean_Meta_isExprDefEq___closed__1 = _init_l_Lean_Meta_isExprDefEq___closed__1(
 lean_mark_persistent(l_Lean_Meta_isExprDefEq___closed__1);
 l_Lean_Meta_isExprDefEq___closed__2 = _init_l_Lean_Meta_isExprDefEq___closed__2();
 lean_mark_persistent(l_Lean_Meta_isExprDefEq___closed__2);
-res = l_Lean_initFn____x40_Lean_Meta_Basic___hyg_13187_(lean_io_mk_world());
+res = l_Lean_initFn____x40_Lean_Meta_Basic___hyg_13207_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));

stage0/stdlib/Lean/Meta/FunInfo.c

@@ -21,13 +21,16 @@ lean_object* lean_mk_empty_array_with_capacity(lean_object*);
 LEAN_EXPORT lean_object* l_Array_qsort_sort___at___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT uint8_t l_Array_contains___at___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps_visit___spec__2(lean_object*, lean_object*);
 lean_object* lean_nat_div(lean_object*, lean_object*);
+lean_object* lean_name_mk_string(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_usize_dec_eq(size_t, size_t);
 lean_object* lean_array_uget(lean_object*, size_t);
+lean_object* l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_getParamNames___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 size_t lean_usize_sub(size_t, size_t);
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
 lean_object* l_Nat_decLt___boxed(lean_object*, lean_object*);
 extern lean_object* l_instInhabitedNat;
+uint8_t l_Lean_Expr_isAppOf(lean_object*, lean_object*);
 static lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___closed__1;
 LEAN_EXPORT lean_object* l_Array_contains___at___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps_visit___spec__2___boxed(lean_object*, lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
@@ -36,7 +39,6 @@ lean_object* l_Std_PersistentHashMap_getCollisionNodeSize___rarg(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_getFunInfo(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_qpartition_loop___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 size_t lean_usize_shift_right(size_t, size_t);
-LEAN_EXPORT lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_nat_add(lean_object*, lean_object*);
 static size_t l_Std_PersistentHashMap_findAux___at___private_Lean_Meta_FunInfo_0__Lean_Meta_checkFunInfoCache___spec__2___closed__1;
@@ -66,8 +68,12 @@ uint64_t lean_uint64_of_nat(lean_object*);
 extern lean_object* l_Lean_instInhabitedExpr;
 size_t lean_usize_mul(size_t, size_t);
 LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps_visit___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-uint8_t l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321_(lean_object*, lean_object*);
+LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1___closed__1;
+static lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1___closed__2;
+uint8_t l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341_(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___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*);
+static lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___closed__1;
 size_t lean_usize_of_nat(lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_whenHasVar___rarg(lean_object*, lean_object*, lean_object*);
 static lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps___closed__1;
@@ -78,6 +84,7 @@ static lean_object* l_Array_qsort_sort___at___private_Lean_Meta_FunInfo_0__Lean_
 LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps_visit___spec__3(lean_object*, lean_object*, size_t, size_t);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps(lean_object*, lean_object*);
 static lean_object* l_Std_PersistentHashMap_insert___at___private_Lean_Meta_FunInfo_0__Lean_Meta_checkFunInfoCache___spec__4___closed__1;
+LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_expr_eqv(lean_object*, lean_object*);
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
 uint8_t lean_usize_dec_le(size_t, size_t);
@@ -100,6 +107,7 @@ LEAN_EXPORT lean_object* l_Std_PersistentHashMap_findAux___at___private_Lean_Met
 LEAN_EXPORT lean_object* l_Array_mapIdxM_map___at___private_Lean_Meta_FunInfo_0__Lean_Meta_updateHasFwdDeps___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at___private_Lean_Meta_FunInfo_0__Lean_Meta_checkFunInfoCache___spec__7(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_usize_to_nat(size_t);
+lean_object* l_Lean_Meta_isProp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Expr_hasFVar(lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps_visit___boxed(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_forallBoundedTelescope___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -128,7 +136,7 @@ else
 {
 lean_object* x_9; uint8_t x_10; 
 x_9 = lean_array_fget(x_1, x_4);
-x_10 = l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321_(x_5, x_9);
+x_10 = l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341_(x_5, x_9);
 lean_dec(x_9);
 if (x_10 == 0)
 {
@@ -198,7 +206,7 @@ lean_inc(x_11);
 x_12 = lean_ctor_get(x_10, 1);
 lean_inc(x_12);
 lean_dec(x_10);
-x_13 = l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321_(x_3, x_11);
+x_13 = l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341_(x_3, x_11);
 lean_dec(x_11);
 if (x_13 == 0)
 {
@@ -409,7 +417,7 @@ else
 {
 lean_object* x_17; uint8_t x_18; 
 x_17 = lean_array_fget(x_5, x_2);
-x_18 = l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321_(x_3, x_17);
+x_18 = l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341_(x_3, x_17);
 lean_dec(x_17);
 if (x_18 == 0)
 {
@@ -506,7 +514,7 @@ if (x_18 == 0)
 lean_object* x_19; lean_object* x_20; uint8_t x_21; 
 x_19 = lean_ctor_get(x_15, 0);
 x_20 = lean_ctor_get(x_15, 1);
-x_21 = l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321_(x_4, x_19);
+x_21 = l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341_(x_4, x_19);
 if (x_21 == 0)
 {
 lean_object* x_22; lean_object* x_23; lean_object* x_24; 
@@ -540,7 +548,7 @@ x_27 = lean_ctor_get(x_15, 1);
 lean_inc(x_27);
 lean_inc(x_26);
 lean_dec(x_15);
-x_28 = l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321_(x_4, x_26);
+x_28 = l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341_(x_4, x_26);
 if (x_28 == 0)
 {
 lean_object* x_29; lean_object* x_30; lean_object* x_31; 
@@ -661,7 +669,7 @@ if (lean_is_exclusive(x_57)) {
  lean_dec_ref(x_57);
  x_62 = lean_box(0);
 }
-x_63 = l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321_(x_4, x_60);
+x_63 = l___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341_(x_4, x_60);
 if (x_63 == 0)
 {
 lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; 
@@ -1972,7 +1980,7 @@ x_8 = lean_unsigned_to_nat(0u);
 x_9 = lean_nat_dec_eq(x_4, x_8);
 if (x_9 == 0)
 {
-lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; uint8_t x_14; lean_object* x_15; lean_object* x_16; 
+lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; uint8_t x_14; lean_object* x_15; uint8_t x_16; uint8_t x_17; lean_object* x_18; 
 x_10 = lean_unsigned_to_nat(1u);
 x_11 = lean_nat_sub(x_4, x_10);
 lean_dec(x_4);
@@ -1981,72 +1989,76 @@ x_13 = lean_ctor_get_uint8(x_12, sizeof(void*)*1);
 x_14 = lean_ctor_get_uint8(x_12, sizeof(void*)*1 + 1);
 x_15 = lean_ctor_get(x_12, 0);
 lean_inc(x_15);
-x_16 = lean_nat_add(x_5, x_10);
+x_16 = lean_ctor_get_uint8(x_12, sizeof(void*)*1 + 2);
+x_17 = lean_ctor_get_uint8(x_12, sizeof(void*)*1 + 3);
+x_18 = lean_nat_add(x_5, x_10);
 if (x_14 == 0)
 {
-uint8_t x_17; 
-x_17 = l_Array_contains___at___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps_visit___spec__2(x_2, x_5);
+uint8_t x_19; 
+x_19 = l_Array_contains___at___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps_visit___spec__2(x_2, x_5);
 lean_dec(x_5);
-if (x_17 == 0)
+if (x_19 == 0)
 {
-lean_object* x_18; 
+lean_object* x_20; 
 lean_dec(x_15);
-x_18 = lean_array_push(x_7, x_12);
+x_20 = lean_array_push(x_7, x_12);
 x_4 = x_11;
-x_5 = x_16;
+x_5 = x_18;
 x_6 = lean_box(0);
-x_7 = x_18;
+x_7 = x_20;
 goto _start;
 }
 else
 {
-uint8_t x_20; 
-x_20 = !lean_is_exclusive(x_12);
-if (x_20 == 0)
+uint8_t x_22; 
+x_22 = !lean_is_exclusive(x_12);
+if (x_22 == 0)
 {
-lean_object* x_21; uint8_t x_22; lean_object* x_23; 
-x_21 = lean_ctor_get(x_12, 0);
-lean_dec(x_21);
-x_22 = 1;
-lean_ctor_set_uint8(x_12, sizeof(void*)*1 + 1, x_22);
-x_23 = lean_array_push(x_7, x_12);
+lean_object* x_23; uint8_t x_24; lean_object* x_25; 
+x_23 = lean_ctor_get(x_12, 0);
+lean_dec(x_23);
+x_24 = 1;
+lean_ctor_set_uint8(x_12, sizeof(void*)*1 + 1, x_24);
+x_25 = lean_array_push(x_7, x_12);
 x_4 = x_11;
-x_5 = x_16;
+x_5 = x_18;
 x_6 = lean_box(0);
-x_7 = x_23;
+x_7 = x_25;
 goto _start;
 }
 else
 {
-uint8_t x_25; lean_object* x_26; lean_object* x_27; 
+uint8_t x_27; lean_object* x_28; lean_object* x_29; 
 lean_dec(x_12);
-x_25 = 1;
-x_26 = lean_alloc_ctor(0, 1, 2);
-lean_ctor_set(x_26, 0, x_15);
-lean_ctor_set_uint8(x_26, sizeof(void*)*1, x_13);
-lean_ctor_set_uint8(x_26, sizeof(void*)*1 + 1, x_25);
-x_27 = lean_array_push(x_7, x_26);
+x_27 = 1;
+x_28 = lean_alloc_ctor(0, 1, 4);
+lean_ctor_set(x_28, 0, x_15);
+lean_ctor_set_uint8(x_28, sizeof(void*)*1, x_13);
+lean_ctor_set_uint8(x_28, sizeof(void*)*1 + 1, x_27);
+lean_ctor_set_uint8(x_28, sizeof(void*)*1 + 2, x_16);
+lean_ctor_set_uint8(x_28, sizeof(void*)*1 + 3, x_17);
+x_29 = lean_array_push(x_7, x_28);
 x_4 = x_11;
-x_5 = x_16;
-x_6 = lean_box(0);
-x_7 = x_27;
-goto _start;
-}
-}
-}
-else
-{
-lean_object* x_29; 
-lean_dec(x_15);
-lean_dec(x_5);
-x_29 = lean_array_push(x_7, x_12);
-x_4 = x_11;
-x_5 = x_16;
+x_5 = x_18;
 x_6 = lean_box(0);
 x_7 = x_29;
 goto _start;
 }
 }
+}
+else
+{
+lean_object* x_31; 
+lean_dec(x_15);
+lean_dec(x_5);
+x_31 = lean_array_push(x_7, x_12);
+x_4 = x_11;
+x_5 = x_18;
+x_6 = lean_box(0);
+x_7 = x_31;
+goto _start;
+}
+}
 else
 {
 lean_dec(x_5);
@@ -2099,6 +2111,45 @@ lean_dec(x_1);
 return x_3;
 }
 }
+static lean_object* _init_l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_mk_string("Decidable");
+return x_1;
+}
+}
+static lean_object* _init_l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1___closed__2() {
+_start:
+{
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = lean_box(0);
+x_2 = l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1___closed__1;
+x_3 = lean_name_mk_string(x_1, x_2);
+return x_3;
+}
+}
+LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_8; uint8_t x_9; lean_object* x_10; lean_object* x_11; 
+x_8 = l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1___closed__2;
+x_9 = l_Lean_Expr_isAppOf(x_2, x_8);
+x_10 = lean_box(x_9);
+x_11 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_11, 0, x_10);
+lean_ctor_set(x_11, 1, x_7);
+return x_11;
+}
+}
+static lean_object* _init_l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1___boxed), 7, 0);
+return x_1;
+}
+}
 LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
 _start:
 {
@@ -2121,85 +2172,197 @@ lean_inc(x_7);
 x_19 = l_Lean_Meta_getFVarLocalDecl(x_18, x_7, x_8, x_9, x_10, x_11);
 if (lean_obj_tag(x_19) == 0)
 {
-lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; uint8_t x_25; uint8_t x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; 
+lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; 
 x_20 = lean_ctor_get(x_19, 0);
 lean_inc(x_20);
 x_21 = lean_ctor_get(x_19, 1);
 lean_inc(x_21);
 lean_dec(x_19);
 x_22 = l_Lean_LocalDecl_type(x_20);
+lean_inc(x_22);
 lean_inc(x_1);
 x_23 = l___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps(x_1, x_22);
 x_24 = l___private_Lean_Meta_FunInfo_0__Lean_Meta_updateHasFwdDeps(x_6, x_23);
 lean_dec(x_6);
-x_25 = l_Lean_LocalDecl_binderInfo(x_20);
+lean_inc(x_10);
+lean_inc(x_9);
+lean_inc(x_8);
+lean_inc(x_7);
+lean_inc(x_22);
+x_25 = l_Lean_Meta_isProp(x_22, x_7, x_8, x_9, x_10, x_21);
+if (lean_obj_tag(x_25) == 0)
+{
+lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; 
+x_26 = lean_ctor_get(x_25, 0);
+lean_inc(x_26);
+x_27 = lean_ctor_get(x_25, 1);
+lean_inc(x_27);
+lean_dec(x_25);
+x_28 = l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___closed__1;
+lean_inc(x_10);
+lean_inc(x_9);
+lean_inc(x_8);
+lean_inc(x_7);
+x_29 = l_Lean_Meta_forallTelescopeReducing___at_Lean_Meta_getParamNames___spec__2___rarg(x_22, x_28, x_7, x_8, x_9, x_10, x_27);
+if (lean_obj_tag(x_29) == 0)
+{
+lean_object* x_30; lean_object* x_31; uint8_t x_32; uint8_t x_33; lean_object* x_34; uint8_t x_35; uint8_t x_36; lean_object* x_37; lean_object* x_38; 
+x_30 = lean_ctor_get(x_29, 0);
+lean_inc(x_30);
+x_31 = lean_ctor_get(x_29, 1);
+lean_inc(x_31);
+lean_dec(x_29);
+x_32 = l_Lean_LocalDecl_binderInfo(x_20);
 lean_dec(x_20);
-x_26 = 0;
-x_27 = lean_alloc_ctor(0, 1, 2);
-lean_ctor_set(x_27, 0, x_23);
-lean_ctor_set_uint8(x_27, sizeof(void*)*1, x_25);
-lean_ctor_set_uint8(x_27, sizeof(void*)*1 + 1, x_26);
-x_28 = lean_array_push(x_24, x_27);
-x_29 = lean_nat_add(x_3, x_5);
+x_33 = 0;
+x_34 = lean_alloc_ctor(0, 1, 4);
+lean_ctor_set(x_34, 0, x_23);
+lean_ctor_set_uint8(x_34, sizeof(void*)*1, x_32);
+lean_ctor_set_uint8(x_34, sizeof(void*)*1 + 1, x_33);
+x_35 = lean_unbox(x_26);
+lean_dec(x_26);
+lean_ctor_set_uint8(x_34, sizeof(void*)*1 + 2, x_35);
+x_36 = lean_unbox(x_30);
+lean_dec(x_30);
+lean_ctor_set_uint8(x_34, sizeof(void*)*1 + 3, x_36);
+x_37 = lean_array_push(x_24, x_34);
+x_38 = lean_nat_add(x_3, x_5);
 lean_dec(x_3);
 x_2 = x_16;
-x_3 = x_29;
-x_6 = x_28;
-x_11 = x_21;
+x_3 = x_38;
+x_6 = x_37;
+x_11 = x_31;
 goto _start;
 }
 else
 {
-uint8_t x_31; 
+uint8_t x_40; 
+lean_dec(x_26);
+lean_dec(x_24);
+lean_dec(x_23);
+lean_dec(x_20);
 lean_dec(x_16);
+lean_dec(x_10);
+lean_dec(x_9);
+lean_dec(x_8);
+lean_dec(x_7);
+lean_dec(x_3);
+lean_dec(x_1);
+x_40 = !lean_is_exclusive(x_29);
+if (x_40 == 0)
+{
+return x_29;
+}
+else
+{
+lean_object* x_41; lean_object* x_42; lean_object* x_43; 
+x_41 = lean_ctor_get(x_29, 0);
+x_42 = lean_ctor_get(x_29, 1);
+lean_inc(x_42);
+lean_inc(x_41);
+lean_dec(x_29);
+x_43 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_43, 0, x_41);
+lean_ctor_set(x_43, 1, x_42);
+return x_43;
+}
+}
+}
+else
+{
+uint8_t x_44; 
+lean_dec(x_24);
+lean_dec(x_23);
+lean_dec(x_22);
+lean_dec(x_20);
+lean_dec(x_16);
+lean_dec(x_10);
+lean_dec(x_9);
+lean_dec(x_8);
+lean_dec(x_7);
+lean_dec(x_3);
+lean_dec(x_1);
+x_44 = !lean_is_exclusive(x_25);
+if (x_44 == 0)
+{
+return x_25;
+}
+else
+{
+lean_object* x_45; lean_object* x_46; lean_object* x_47; 
+x_45 = lean_ctor_get(x_25, 0);
+x_46 = lean_ctor_get(x_25, 1);
+lean_inc(x_46);
+lean_inc(x_45);
+lean_dec(x_25);
+x_47 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_47, 0, x_45);
+lean_ctor_set(x_47, 1, x_46);
+return x_47;
+}
+}
+}
+else
+{
+uint8_t x_48; 
+lean_dec(x_16);
+lean_dec(x_10);
+lean_dec(x_9);
+lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_3);
 lean_dec(x_1);
-x_31 = !lean_is_exclusive(x_19);
-if (x_31 == 0)
+x_48 = !lean_is_exclusive(x_19);
+if (x_48 == 0)
 {
 return x_19;
 }
 else
 {
-lean_object* x_32; lean_object* x_33; lean_object* x_34; 
-x_32 = lean_ctor_get(x_19, 0);
-x_33 = lean_ctor_get(x_19, 1);
-lean_inc(x_33);
-lean_inc(x_32);
+lean_object* x_49; lean_object* x_50; lean_object* x_51; 
+x_49 = lean_ctor_get(x_19, 0);
+x_50 = lean_ctor_get(x_19, 1);
+lean_inc(x_50);
+lean_inc(x_49);
 lean_dec(x_19);
-x_34 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_34, 0, x_32);
-lean_ctor_set(x_34, 1, x_33);
-return x_34;
+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;
 }
 }
 }
 else
 {
-lean_object* x_35; 
+lean_object* x_52; 
+lean_dec(x_10);
+lean_dec(x_9);
+lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_35 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_35, 0, x_6);
-lean_ctor_set(x_35, 1, x_11);
-return x_35;
+x_52 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_52, 0, x_6);
+lean_ctor_set(x_52, 1, x_11);
+return x_52;
 }
 }
 else
 {
-lean_object* x_36; 
+lean_object* x_53; 
+lean_dec(x_10);
+lean_dec(x_9);
+lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_3);
 lean_dec(x_2);
 lean_dec(x_1);
-x_36 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_36, 0, x_6);
-lean_ctor_set(x_36, 1, x_11);
-return x_36;
+x_53 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_53, 0, x_6);
+lean_ctor_set(x_53, 1, x_11);
+return x_53;
 }
 }
 }
@@ -2341,7 +2504,7 @@ static lean_object* _init_l___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoA
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_alloc_closure((void*)(l___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___lambda__1___boxed), 7, 0);
+x_1 = lean_alloc_closure((void*)(l___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___lambda__1), 7, 0);
 return x_1;
 }
 }
@@ -3358,30 +3521,30 @@ return x_265;
 }
 }
 }
+LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_8; 
+x_8 = l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_8;
+}
+}
 LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
 _start:
 {
 lean_object* x_12; 
 x_12 = l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
-lean_dec(x_10);
-lean_dec(x_9);
-lean_dec(x_8);
 lean_dec(x_5);
 lean_dec(x_4);
 return x_12;
 }
 }
-LEAN_EXPORT lean_object* l___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
-_start:
-{
-lean_object* x_8; 
-x_8 = l___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
-lean_dec(x_6);
-lean_dec(x_5);
-lean_dec(x_4);
-return x_8;
-}
-}
 LEAN_EXPORT lean_object* l_Lean_Meta_getFunInfo(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
@@ -3446,6 +3609,12 @@ l_Array_qsort_sort___at___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps___s
 lean_mark_persistent(l_Array_qsort_sort___at___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps___spec__1___closed__1);
 l___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps___closed__1 = _init_l___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps___closed__1();
 lean_mark_persistent(l___private_Lean_Meta_FunInfo_0__Lean_Meta_collectDeps___closed__1);
+l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1___closed__1 = _init_l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1___closed__1();
+lean_mark_persistent(l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1___closed__1);
+l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1___closed__2 = _init_l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1___closed__2();
+lean_mark_persistent(l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___lambda__1___closed__2);
+l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___closed__1 = _init_l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___closed__1();
+lean_mark_persistent(l_Std_Range_forIn_loop___at___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___spec__1___closed__1);
 l___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___closed__1 = _init_l___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___closed__1();
 lean_mark_persistent(l___private_Lean_Meta_FunInfo_0__Lean_Meta_getFunInfoAux___closed__1);
 return lean_io_result_mk_ok(lean_box(0));

stage0/stdlib/Lean/Meta/WHNF.c

@@ -90,6 +90,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_getStuckMVar_x3f(lean_object*, lean_object*
 static lean_object* l_Lean_Meta_toCtorIfLit___closed__5;
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_getConstNoEx_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Meta_markSmartUnfoldingMatchAlt___closed__2;
 LEAN_EXPORT lean_object* l_Lean_Meta_withNatValue___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_whnfEasyCases___closed__5;
 LEAN_EXPORT lean_object* l___private_Lean_Meta_WHNF_0__Lean_Meta_cached_x3f(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -106,6 +107,7 @@ static lean_object* l_Lean_Meta_toCtorIfLit___closed__10;
 LEAN_EXPORT uint8_t l___private_Lean_Meta_WHNF_0__Lean_Meta_getRecRuleFor___lambda__1(lean_object*, lean_object*);
 uint8_t l_Lean_Expr_isAppOf(lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_reduceNative_x3f___closed__5;
+static lean_object* l_Lean_Meta_markSmartUnfoldingMatchAlt___closed__1;
 lean_object* lean_expr_instantiate1(lean_object*, lean_object*);
 lean_object* l_Array_toSubarray___rarg(lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_reduceNat_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -116,7 +118,6 @@ static lean_object* l_Lean_Meta_whnfEasyCases___closed__3;
 LEAN_EXPORT lean_object* l_Lean_List_toExprAux___at_Lean_Meta_toCtorIfLit___spec__1(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_reduceBinNatOp___closed__13;
 LEAN_EXPORT lean_object* l___private_Lean_Meta_WHNF_0__Lean_Meta_reduceQuotRec(lean_object*);
-LEAN_EXPORT lean_object* l_Lean_Meta_markSmartUnfoldigMatchAlt(lean_object*);
 lean_object* l_Lean_Meta_getConst_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_unfoldDefinition_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_whnfEasyCases___at_Lean_Meta_whnfUntil___spec__2___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -185,7 +186,6 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_toCtorIfLit___closed__15;
 LEAN_EXPORT lean_object* l___private_Lean_Meta_WHNF_0__Lean_Meta_getRecRuleFor___boxed(lean_object*, lean_object*);
 static lean_object* l___private_Lean_Meta_WHNF_0__Lean_Meta_canUnfoldAtMatcher___closed__27;
-static lean_object* l_Lean_Meta_markSmartUnfoldigMatchAlt___closed__1;
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Meta_reduceBoolNativeUnsafe___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l___private_Lean_Meta_WHNF_0__Lean_Meta_useWHNFCache(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Meta_markSmartUnfoldingMatch___closed__2;
@@ -246,7 +246,6 @@ static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_WHNF___hyg_24____closed_
 lean_object* l_Lean_Meta_getDelayedAssignment_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Std_Range_forIn_loop___at___private_Lean_Meta_WHNF_0__Lean_Meta_toCtorWhenStructure___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*);
 static lean_object* l___private_Lean_Meta_WHNF_0__Lean_Meta_canUnfoldAtMatcher___closed__30;
-static lean_object* l_Lean_Meta_markSmartUnfoldigMatchAlt___closed__2;
 static lean_object* l_Lean_Meta_whnfEasyCases___at_Lean_Meta_whnfCore___spec__3___lambda__3___closed__1;
 static lean_object* l_Lean_Meta_whnfEasyCases___at_Lean_Meta_whnfCore___spec__3___lambda__3___closed__2;
 static lean_object* l_Lean_Meta_reduceNat_x3f___closed__19;
@@ -413,6 +412,7 @@ lean_object* l___private_Lean_Expr_0__Lean_mkAppRangeAux(lean_object*, lean_obje
 lean_object* lean_expr_abstract(lean_object*, lean_object*);
 static lean_object* l_Lean_List_toExprAux___at_Lean_Meta_toCtorIfLit___spec__1___closed__5;
 LEAN_EXPORT lean_object* l_Lean_Meta_reduceNat_x3f___lambda__1___boxed(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Meta_markSmartUnfoldingMatchAlt(lean_object*);
 static lean_object* l_Lean_Meta_reduceBinNatOp___closed__8;
 LEAN_EXPORT lean_object* l_Lean_Meta_reduceBinNatOp___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Meta_whnfEasyCases___at_Lean_Meta_whnfImp___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -659,7 +659,7 @@ lean_dec(x_1);
 return x_2;
 }
 }
-static lean_object* _init_l_Lean_Meta_markSmartUnfoldigMatchAlt___closed__1() {
+static lean_object* _init_l_Lean_Meta_markSmartUnfoldingMatchAlt___closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -667,21 +667,21 @@ x_1 = lean_mk_string("sunfoldMatchAlt");
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Meta_markSmartUnfoldigMatchAlt___closed__2() {
+static lean_object* _init_l_Lean_Meta_markSmartUnfoldingMatchAlt___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Meta_markSmartUnfoldigMatchAlt___closed__1;
+x_2 = l_Lean_Meta_markSmartUnfoldingMatchAlt___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Meta_markSmartUnfoldigMatchAlt(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_Meta_markSmartUnfoldingMatchAlt(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
-x_2 = l_Lean_Meta_markSmartUnfoldigMatchAlt___closed__2;
+x_2 = l_Lean_Meta_markSmartUnfoldingMatchAlt___closed__2;
 x_3 = l_Lean_mkAnnotation(x_2, x_1);
 return x_3;
 }
@@ -690,7 +690,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_smartUnfoldingMatchAlt_x3f(lean_object* x_1
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
-x_2 = l_Lean_Meta_markSmartUnfoldigMatchAlt___closed__2;
+x_2 = l_Lean_Meta_markSmartUnfoldingMatchAlt___closed__2;
 x_3 = l_Lean_annotation_x3f(x_2, x_1);
 return x_3;
 }
@@ -30246,10 +30246,10 @@ lean_dec_ref(res);
 lean_mark_persistent(l_Lean_Meta_markSmartUnfoldingMatch___closed__1);
 l_Lean_Meta_markSmartUnfoldingMatch___closed__2 = _init_l_Lean_Meta_markSmartUnfoldingMatch___closed__2();
 lean_mark_persistent(l_Lean_Meta_markSmartUnfoldingMatch___closed__2);
-l_Lean_Meta_markSmartUnfoldigMatchAlt___closed__1 = _init_l_Lean_Meta_markSmartUnfoldigMatchAlt___closed__1();
-lean_mark_persistent(l_Lean_Meta_markSmartUnfoldigMatchAlt___closed__1);
-l_Lean_Meta_markSmartUnfoldigMatchAlt___closed__2 = _init_l_Lean_Meta_markSmartUnfoldigMatchAlt___closed__2();
-lean_mark_persistent(l_Lean_Meta_markSmartUnfoldigMatchAlt___closed__2);
+l_Lean_Meta_markSmartUnfoldingMatchAlt___closed__1 = _init_l_Lean_Meta_markSmartUnfoldingMatchAlt___closed__1();
+lean_mark_persistent(l_Lean_Meta_markSmartUnfoldingMatchAlt___closed__1);
+l_Lean_Meta_markSmartUnfoldingMatchAlt___closed__2 = _init_l_Lean_Meta_markSmartUnfoldingMatchAlt___closed__2();
+lean_mark_persistent(l_Lean_Meta_markSmartUnfoldingMatchAlt___closed__2);
 l_Lean_Meta_isAuxDef___closed__1 = _init_l_Lean_Meta_isAuxDef___closed__1();
 lean_mark_persistent(l_Lean_Meta_isAuxDef___closed__1);
 l___private_Lean_Meta_WHNF_0__Lean_Meta_mkNullaryCtor___closed__1 = _init_l___private_Lean_Meta_WHNF_0__Lean_Meta_mkNullaryCtor___closed__1();

stage0/stdlib/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.c

@@ -298,6 +298,7 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze_analyzeApp___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_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyzeAppStagedCore_analyzeArg___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_EXPORT lean_object* l_panic___at_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze_analyzeMData___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1(lean_object*, lean_object*);
 static lean_object* l_Lean_PrettyPrinter_Delaborator_initFn____x40_Lean_PrettyPrinter_Delaborator_TopDownAnalyze___hyg_9461____closed__1;
 static lean_object* l_Lean_initFn____x40_Lean_PrettyPrinter_Delaborator_TopDownAnalyze___hyg_205____closed__4;
 static lean_object* l_panic___at_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze_analyzeConst___spec__1___closed__1;
@@ -598,7 +599,6 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_isHBinOp___l
 static lean_object* l_Lean_initFn____x40_Lean_PrettyPrinter_Delaborator_TopDownAnalyze___hyg_289____closed__3;
 static lean_object* l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_isTrivialBottomUp___closed__7;
 static lean_object* l_Lean_initFn____x40_Lean_PrettyPrinter_Delaborator_TopDownAnalyze___hyg_261____closed__4;
-uint8_t l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_canBottomUp___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_getPPProofs(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyzeAppStagedCore_analyzeArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -3546,7 +3546,7 @@ lean_inc(x_4);
 lean_dec(x_1);
 x_5 = lean_alloc_ctor(1, 1, 0);
 lean_ctor_set(x_5, 0, x_4);
-x_6 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_321____spec__1(x_3, x_5);
+x_6 = l___private_Init_Data_Option_Basic_0__beqOption____x40_Init_Data_Option_Basic___hyg_800____at___private_Lean_Meta_Basic_0__Lean_Meta_beqInfoCacheKey____x40_Lean_Meta_Basic___hyg_341____spec__1(x_3, x_5);
 lean_dec(x_5);
 lean_dec(x_3);
 return x_6;