以下の内容はhttps://m-hiyama-memo.hatenablog.com/entry/2023/02/27/135636より取得しました。


casesのケースの順序

def toNum (b : Bool) : Nat := by
  cases b with
  | true => exact 1
  | false => exact 0
#print toNum
#print Bool.casesOn
#eval toNum true --> 1

def toNum' (b : Bool) : Nat := by
  cases b 
  exact 1
  exact 0
#eval toNum' true --> 0

def toNum'' (b : Bool) : Nat := by
  cases b 
  · exact 1
  · exact 0
#eval toNum'' true --> 0

インフォビューを見てないと順番がわからない。cases/with使ったほうがいいな。




以上の内容はhttps://m-hiyama-memo.hatenablog.com/entry/2023/02/27/135636より取得しました。
このページはhttp://font.textar.tv/のウェブフォントを使用してます

不具合報告/要望等はこちらへお願いします。
モバイルやる夫Viewer Ver0.14