#reduce
#reduce
は、与えられた式をこれ以上簡約できなくなるまで簡約します。
/-- info: 4 -/
#guard_msgs in #reduce 1 + 3
/-- info: 4 -/
#guard_msgs in #reduce (fun x => x + 1) 3
これだけ見ると #eval
と同じですが、#reduce
は式の評価ではなくて簡約なので、関数や型も渡すことができます。
def addOne (x : Nat) := x + 1
-- addOne が定義に展開されている
/-- info: fun x => x.succ -/
#guard_msgs in #reduce addOne
-- 合成が計算できる
/-- info: fun x => x.succ.succ -/
#guard_msgs in #reduce addOne ∘ addOne