I am wondering, if the Church-Turing thesis holds (all effectively calculable functions are computable by Turing machines/lambda calculus) and I can compute the limit of a function by hand, what is the encoding of e.g. the derivative $\lim_{h\to 0} \frac{df(x)}{dh} = \frac{f(x+h)-f(x)}{h}$.
I know the encoding for the divide and plus sequences, but how would one encode the limit?