In what order are chained implications evaluated? (i.e. $a \implies b \implies c$) Implication does not appear to be associative:
a  b  c | (a -> b) -> c | a -> (b -> c)
F  T  F | F             | T
F  F  F | F             | T

Is $a \implies b \implies c$ evaluated as $a \implies (b \implies c)$ or $(a \implies b) \implies c$?

In computer science, the convention that $a \to b \to c$ means $a \to (b\to c)$ is near universal -- because, through the Curry-Howard isomorphism, such formulas correspond to useful curried types in functional languages.
