In a total language, you can prove that `even(n+n) = true`. Dhall probably doesn’t bother with this because it’s focused on proving that your resulting data str

In a total language, you can prove that `even(n+n) = true`. Dhall probably doesn’t bother with this because it’s focused on proving that your resulting data structures are equivalent: so, since functions are guaranteed to run in a bounded amount of time, it just runs all the functions it finds and then normalizes the resulting data structure. Equality between these data structures implies program equivalence.