Proof by example that lean is much better at verifying simple proof terms than doing recursive computations in the kernel using decide. #time says it takes 7 seconds, but because it is checked twice as written (once in the kernel and once in the elaborator) half of this time could be eliminated with some additional work.
Proof by example that lean is much better at verifying simple proof terms than doing recursive computations in the kernel using
decide.#timesays it takes 7 seconds, but because it is checked twice as written (once in the kernel and once in the elaborator) half of this time could be eliminated with some additional work.