search

lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
39 stars 7 forks source link

コード例: for ループの範囲から情報を取り出す方法 #444

Closed Seasawher closed 1 month ago

Seasawher commented 3 months ago

下記の状況で sorry の証明が埋められることは人間には明らかだが，Lean にこれをわかってもらうにはどうしたらいい？

def m := 10

def main : IO Unit :=
  for i in [0:m] do
    let i : Fin m := ⟨i, by sorry⟩
    IO.println i

#eval main
Seasawher commented 3 months ago

Zulip: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/get.20info.20from.20the.20range.20of.20.60for.60/near/449046936

Seasawher commented 3 months ago

これで行ける

def m := 10

def main : IO Unit :=
  for h : i in [0:m] do
    let i : Fin m := ⟨i, h.right⟩
    IO.println i

#eval main