Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
doc: code comments about reflection support (#5235)
I found that the kernel has special support for `e =?= true`, and will in this case aggressively whnf `e`. This explains the following behavior (for a `sqrt` function with fuel): ```lean theorem foo : sqrt 100000000000000000002 == 10000000000 := rfl -- fast theorem foo : sqrt 100000000000000000002 = 10000000000 := rfl -- slow theorem foo : sqrt 100000000000000000002 = 10000000000 := by decide -- fast ``` The special support in the kernel only applies for closed `e` and `true` on the RHS. It could be generlized (also open terms, also `false`, other data type's constructors, different orientation). But maybe I should wait for evidence that this generaziation really matters, or whether all applications (proof by reflection) can be made to have this form.
- Loading branch information