`lim[x->0] (cos(x) - 1) / x` incorrectly returns `NaN`

[jackmaney]

Hi guys,thank you for using Hilbert.
You need to execute "postulate zfc_analysis" if you wanna do real analysis.

Enjoy! -> postulate zfc_analysis
success! :)
Enjoy! -> lim[x->0] (cos(x) - 1) / x
NaN
Enjoy! ->

By L'Hospital's Rule (and using the notation within Hilbert):

lim[x->0] (cos(x) - 1) / x == lim[x->0] -sin(x) / 1 == 0

[jackmaney]

Hi guys,thank you for using Hilbert.
You need to execute "postulate zfc_analysis" if you wanna do real analysis.

Enjoy! -> postulate zfc_analysis
success! :)
Enjoy! -> lim[x->0] (x^2)^x
0.0
Enjoy! ->

This is incorrect, as the value of the limit is 1 (since log(x^(2*x)) = 2*x*log(x) approaches 0 as x approaches 0).