rflタクティク

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 0

A = A の形でないとターゲットに適用できない。カーネルによる還元計算はしてくれるが、カーネルの計算がどこまでやってくれるかがイマイチわからない。