構造体の継承について詳細を補足する

structure MythicalCreature where
  large : Bool
deriving Repr

inductive Size where
  | small
  | medium
  | large
deriving BEq, Repr

structure SizedCreature extends MythicalCreature where
  size : Size
  large := size == Size.large
deriving Repr

-- size を渡すだけで SizedCreature が作れる
#eval {size := .small, large := false : SizedCreature}
#eval {size := .small : SizedCreature}

-- where でも省略できる
def sample : SizedCreature where
  size := .small

-- コンストラクタにおいて large にデフォルト値が与えられるわけではない
#check SizedCreature.mk (size := .small)

-- 明示的に渡すこともできる
def nonsenseCreature : SizedCreature where
  large := false
  size := .large

#check BEq
#print Hashable

abbrev SizesMatch (sc : SizedCreature) : Prop :=
  sc.large = (sc.size == Size.large)

def huldre : SizedCreature where
  size := .medium

example : SizesMatch huldre := by
  simp [huldre]

No target file or test is named in the issue. Start by locating the existing documentation about Lean structure extension and read or run the provided examples. Done means the documentation explains the inheritance, default field, constructor, and proof examples shown here.