昨日の関数合成はなんか違ったかも…….でもよくわかってない.
import Mathlib.Tactic
open Nat
@[simp]
def fun_pow {α : Type u} (f : α → α) : (n : Nat) → (α → α)
| 0 => id
| succ n => (fun_pow f n) ∘ f
instance {α : Type u} : HPow (α → α) (Nat) (α → α) where
hPow := fun_pow
def f : (Fin 2) → (Fin 2)
| 0 => 1
| 1 => 0
theorem a {α : Type u} (g : α → α) : g^(0) = id := by rfl
theorem aa : f^(0) = id := by
rfl
最後のrflが通らない.simpすると1 = idとかに簡略化されてしまっているらしい.何だろう.うーむ.最初のimportがないと動くような.
0 件のコメント:
コメントを投稿
コメントの追加にはサードパーティーCookieの許可が必要です