constructor タクティクで任意の構造体を分解する例を示す

[Seasawher]

structure Sample where
  name : String
  index : Nat

def getSample (index : Nat) (name : String) : Sample := by
  -- constructor タクティクでゴールの構造体をフィールドに分解する
  constructor

  · exact name
  · exact index