Lean4 で print デバッグをする

プログラムにバグがあったとき，関数の途中で変数に何が入っているのか確かめたくなるのが人情というものです．

Python だったら print 関数を使うところですが，Lean Prover でそれをするには dbg_trace というコマンドが用意されています．

試しに Fibonacci 数列の指数時間と線形時間の実装に対して，それぞれ n での値を計算するのに再帰呼び出しがどのように行われているのか見てみましょう．