If we equate haskells Int type to a mathematical integer, then (loop 0) -> 1 + 1 + ... 1 + 1 + ... = 1 + (1 + 1 + ...) We can still use equational reasoning,

If we equate haskells Int type to a mathematical integer, then (loop 0) -> 1 + 1 + ... 1 + 1 + ... = 1 + (1 + 1 + ...) We can still use equational reasoning, it's just that equational reasoning is different for divergent non-terminating equations