2023-02-27 rflタクティク Lean 具体例 rflは exact Eq.refl 項 の略記。適切な項は見つけてくれる。 theorem t1 (y : Nat) : (fun x : Nat => 0) y = 0 := by rfl theorem t2 (y : Nat) : (fun x : Nat => 0) y = 0 := by exact Eq.refl 0A = A の形でないとターゲットに適用できない。カーネルによる還元計算はしてくれるが、カーネルの計算がどこまでやってくれるかがイマイチわからない。