It might also be useful to have an operation like `something_satisfying : (number -> bool) -> number`.
This should be possible, but it would require some thought to implement correctly.

It would also be useful to have an operation like `something_satisfying : (number -> bool) -> number`, but it would require some thought to implement correctly.

(=), (<), (>), (<=), (>=) : number -> number -> bool
(&&), (||) : bool -> bool -> bool

(<), (>), (<=), (>=) : number -> number -> bool
(=) : a -> a -> bool
(&&), (||), (=>) : bool -> bool -> bool

forall, exists : (number -> bool) -> bool
something_satisfying : (number -> bool) -> number

Useful derived functions:

Some useful derived functions:

{-
    If you graph `x, y => y = x^2`, the result will be invisible, because it's an infinitely thin curve.
    If you graph `holds_within 0.1 (x, y => y = x^2)`, the result will be a curve of width 0.2, so you can actually see it.
-}

-- Useful for thickening lines, so they are actually visible on the graph.

abs : number -> number
abs x = if (x < 0) (-x) x
-- The limit of f as its input goes to zero.
limit : (number -> number) -> number
limit x f = 
    something_satisfying (l -> 
        ∀ε. ε > 0 => 
            ∃δ. δ > 0 && 
                ∀x. abs x < δ => 
                    abs (f x - l) < ε
    )
derivative : (number -> number) -> (number -> number)
derivative f x = limit (dx -> (f (x+dx) - f x) / dx)

For efficiency reasons, limit should be implemented as a primitive, if possible.

If it were, trig functions could be defined like this:
\\[
    \\begin{align*}
    & \\exists \\sin. \\exists \\cos. \\\\
    & \\quad \\cos 0 = 1 \\ \\land \\\\
    & \\quad \\sin 0 = 0 \\ \\land \\\\
    & \\quad (\\forall x. \\forall \\epsilon. \\epsilon > 0 \\implies \\\\
    & \\qquad \\exists \\delta. \\delta > 0 \\ \\land \\\\
    & \\qquad \\quad \\forall y. |y - x| < \\delta \\implies \\\\
    & \\qquad \\qquad |(\\sin y - \\sin x) / (y - x) - \\cos x| < \\epsilon \\ \\land \\\\
    & \\qquad \\qquad |(\\cos y - \\cos x) / (y - x) + \\sin x| < \\epsilon \\\\
    & \\quad ) \\ \\land \\\\
    & \\quad \\textit{rest of expression} \\\\
    & \\end{align*}
\\]
(Yes, I'm using the epsilon-delta definition of derivative to describe differential equations.)

If you have trig functions, you can define the natural numbers:
\\[\\text{is_natural}(x) = x \\geq 0 \\land \\exists \\pi. \\pi > 3 \\land \\pi < 4 \\land \\sin \\pi = 0 \\land \\sin \\pi x = 0\\]

If it were, the integers could be defined as follows:
```text
is_integer : number -> bool
is_integer n = 
    ∃sin. ∃cos. 
        cos 0 = 1 && sin 0 = 0 && 
        derivative sin = cos && derivative cos = (x -> -sin x)) &&
        ∃π. π > 3 && π < 4 && sin π = 0 &&
            sin (π*n) = 0
```

And then you can use standard Godelian tricks to create a paradox.

And then you could use standard Godelian tricks to create a paradox.