#reduce

#reduce は、与えられた式をこれ以上簡約できなくなるまで簡約します。

/- info: 4 -/
#reduce 1 + 3

/- info: 4 -/
#reduce (fun x => x + 1) 3

これだけ見ると #eval と同じですが、#reduce は式の評価ではなくて簡約なので、関数や型も渡すことができます。

section
  /- ## 関数を渡す例 -/

  def addOne (x : Nat) := x + 1

  -- addOne が定義に展開されている
  /- info: fun x => x.succ -/
  #reduce addOne

  -- 合成が計算できる
  /- info: fun x => x.succ.succ -/
  #reduce addOne ∘ addOne
end

section
  /- ## 型を渡す例 -/

  def Natural (n : Nat) : Type :=
    match n with
    | 0 => Nat
    | n + 1 => Natural n → Nat

  -- 全く簡約されない
  /- info: Natural 0 -/
  #reduce Natural 0
end