Defining the Implies function whilst hiding it from the rendered
document makes following the chapter difficult, as the reader expects
that it is a built-in alongside the other propositional connectives.
This patch also makes explicit the definition for Proof for the same
reason: without the definition one can't follow along in an editor. I wonder
if for pedagogical purposes defining it as an axiom rather than a structure
is less opaque?
Defining the
Impliesfunction whilst hiding it from the rendered document makes following the chapter difficult, as the reader expects that it is a built-in alongside the other propositional connectives.This patch also makes explicit the definition for
Prooffor the same reason: without the definition one can't follow along in an editor. I wonder if for pedagogical purposes defining it as anaxiomrather than astructureis less opaque?