Lean.Meta.Structure

Equations

Lean.Meta.getStructureName struct = match Lean.Expr.getAppFn struct with | Lean.Expr.const declName x x_1 => do let a ← Lean.getEnv let _do_jp : PUnit → Lean.MetaM Lean.Name := fun y => pure declName if Lean.isStructure a declName = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "'" ++ Lean.toMessageData declName ++ Lean.toMessageData "' is not a structure") _do_jp y | x => Lean.throwError (Lean.toMessageData "expected structure")