def Lean.Meta.Grind.Arith.Linear.getStructId? (type : Expr) : GoalM (Option Nat)

def Lean.Meta.Grind.Arith.Linear.getStructId?.go? (type : Expr) : GoalM (Option Nat)

def Lean.Meta.Grind.Arith.Linear.getStructId?.go?.getInst? (type : Expr) (u : Level) (declName : Name) : GoalM (Option Expr)

def Lean.Meta.Grind.Arith.Linear.getStructId?.go?.getInst (type : Expr) (u : Level) (declName : Name) : GoalM Expr

def Lean.Meta.Grind.Arith.Linear.getStructId?.go?.getBinHomoInst (type : Expr) (u : Level) (declName : Name) : GoalM Expr

def Lean.Meta.Grind.Arith.Linear.getStructId?.go?.getHMulIntInst (type : Expr) (u : Level) : GoalM Expr

def Lean.Meta.Grind.Arith.Linear.getStructId?.go?.getHMulNatInst (type : Expr) (u : Level) : GoalM Expr

def Lean.Meta.Grind.Arith.Linear.getStructId?.go?.checkToFieldDefEq? (type : Expr) (u : Level) (parentInst? inst? : Option Expr) (toFieldName : Name) : GoalM (Option Expr)

def Lean.Meta.Grind.Arith.Linear.getStructId?.go?.ensureToFieldDefEq (type : Expr) (u : Level) (parentInst inst : Expr) (toFieldName : Name) : GoalM Unit

def Lean.Meta.Grind.Arith.Linear.getStructId?.go?.ensureToHomoFieldDefEq (type : Expr) (u : Level) (parentInst inst : Expr) (toFieldName toHeteroName : Name) : GoalM Unit

def Lean.Meta.Grind.Arith.Linear.getStructId?.go?.getHSMulFn? (type : Expr) (u : Level) : GoalM (Option Expr)

def Lean.Meta.Grind.Arith.Linear.getStructId?.go?.getHSMulNatFn? (type : Expr) (u : Level) : GoalM (Option Expr)

def Lean.Meta.Grind.Arith.Linear.getStructId?.go?.getOne? (type : Expr) (u : Level) : GoalM (Option Expr)

def Lean.Meta.Grind.Arith.Linear.getStructId?.go?.getNoNatZeroDivInst? (type : Expr) (u : Level) : GoalM (Option Expr)