【Lean4】use

Lean4

2026.07.22

use

存在命題の証人を指定する

Plaintext

example : ∃ n : ℕ, n = 3 := by
  use 3

example : ∃ n : ℕ, n = 3 := by
  use 3

タイトルとURLをコピーしました