fix: isStructure vs isStructureLike

src/Init/Core.lean

@@ -446,8 +446,8 @@ class inductive Nonempty (α : Sort u) : Prop where
 protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
   h₂ h₁.1
 
-instance {α : Sort u} [Inhabited α] : Nonempty α where
-  val := arbitrary
+instance {α : Sort u} [Inhabited α] : Nonempty α :=
+  ⟨arbitrary⟩
 
 theorem nonemptyOfExists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α
   | ⟨w, h⟩ => ⟨w⟩

src/Lean/Elab/App.lean

@@ -502,7 +502,7 @@ private partial def findMethod? (env : Environment) (structName fieldName : Name
     match env.find? fullNamePrv with
     | some _ => some (structName, fullNamePrv)
     | none   =>
-      if isStructureLike env structName then
+      if isStructure env structName then
         (getParentStructures env structName).findSome? fun parentStructName => findMethod? env parentStructName fieldName
       else
         none
@@ -515,16 +515,17 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     let env ← getEnv
     unless isStructureLike env structName do
       throwLValError e eType "invalid projection, structure expected"
-    let fieldNames := getStructureFields env structName
-    if h : idx - 1 < fieldNames.size then
+    let numFields := getStructureLikeNumFields env structName
+    if idx - 1 < numFields then
       if isStructure env structName then
-        return LValResolution.projFn structName structName (fieldNames.get ⟨idx - 1, h⟩)
+        let fieldNames := getStructureFields env structName
+        return LValResolution.projFn structName structName fieldNames[idx - 1]
       else
         /- `structName` was declared using `inductive` command.
            So, we don't projection functions for it. Thus, we use `Expr.proj` -/
         return LValResolution.projIdx structName (idx - 1)
     else
-      throwLValError e eType m!"invalid projection, structure has only {fieldNames.size} field(s)"
+      throwLValError e eType m!"invalid projection, structure has only {numFields} field(s)"
   | some structName, LVal.fieldName _ fieldName _ _ =>
     let env ← getEnv
     let searchEnv : Unit → TermElabM LValResolution := fun _ => do

src/Lean/Elab/StructInst.lean

@@ -812,7 +812,7 @@ end DefaultFields
 
 private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (source : Source) : TermElabM Expr := do
   let (structName, structType) ← getStructName stx expectedType? source
-  unless isStructureLike (← getEnv) structName do
+  unless isStructure (← getEnv) structName do
     throwError "invalid \{...} notation, structure type expected{indentExpr structType}"
   let struct ← liftMacroM <| mkStructView stx structName source
   let struct ← expandStruct struct

src/Lean/Meta/AppBuilder.lean

@@ -358,7 +358,7 @@ partial def mkProjection : Expr → Name → MetaM Expr
     match type.getAppFn with
     | Expr.const structName us _ =>
       let env ← getEnv
-      unless isStructureLike env structName do
+      unless isStructure env structName do
         throwAppBuilderException `mkProjection ("structure expected" ++ hasTypeMsg s type)
       match getProjFnForField? env structName fieldName with
       | some projFn =>

src/Lean/Server/Completion.lean

@@ -211,7 +211,7 @@ where
     match type.getAppFn with
     | Expr.const typeName .. =>
       modify fun s => s.insert typeName
-      if isStructureLike (← getEnv) typeName then
+      if isStructure (← getEnv) typeName then
         for parentName in getAllParentStructures (← getEnv) typeName do
           modify fun s => s.insert parentName
       let type? ← try unfoldDefinition? type catch _ => pure none

src/Lean/Structure.lean

@@ -57,14 +57,6 @@ def getStructureInfo? (env : Environment) (structName : Name) : Option Structure
   | some modIdx => structureExt.getModuleEntries env modIdx |>.binSearch { structName } StructureInfo.lt
   | none        => structureExt.getState env |>.map.find? structName
 
-/--
-  Return true iff `constName` is the a non-recursive inductive
-  datatype that has only one constructor. -/
-def isStructureLike (env : Environment) (constName : Name) : Bool :=
-  match env.find? constName with
-  | some (ConstantInfo.inductInfo { isRec := false, ctors := [ctor], .. }) => true
-  | _ => false
-
 /-- We mark subobject fields by prefixing them with "_" in the structure's intro rule. -/
 def mkInternalSubobjectFieldName (fieldName : Name) : Name :=
   fieldName.appendBefore "_"
@@ -174,4 +166,19 @@ partial def getPathToBaseStructureAux (env : Environment) (baseStructName : Name
 def getPathToBaseStructure? (env : Environment) (baseStructName : Name) (structName : Name) : Option (List Name) :=
   getPathToBaseStructureAux env baseStructName structName []
 
+/-- Return true iff `constName` is the a non-recursive inductive datatype that has only one constructor. -/
+def isStructureLike (env : Environment) (constName : Name) : Bool :=
+  match env.find? constName with
+  | some (ConstantInfo.inductInfo { isRec := false, ctors := [ctor], .. }) => true
+  | _ => false
+
+/-- Return number of fields for a structure-like type -/
+def getStructureLikeNumFields (env : Environment) (constName : Name) : Nat :=
+  match env.find? constName with
+  | some (ConstantInfo.inductInfo { isRec := false, ctors := [ctor], .. }) =>
+    match env.find? ctor with
+    | some (ConstantInfo.ctorInfo { numFields := n, .. }) => n
+    | _ => 0
+  | _ => 0
+
 end Lean