3 ms·

> Will the string "(n : nat) : 0 + n = n" appear in this list? No, because the given alphabet does not contain the space character ...

• jamesfisher 4y ago
  Thank you for your precise eyes! Fixed!
  • evnp 4y ago
    Similar nit, when you ask "Will theorems() discover `theorem halting_problem (n) : ¬ computable_pred (λ c, ..." I don't believe it will since `const alphabet` does not contain λ or ¬. Apart from my very slight indignance after answering that one incorrectly, loved the article! :)
  • auggierose 4y ago
    Great tutorial, by the way! There is another typo in one of the javascript functions, where you should write "return t;" instead of "return thm;"
    • martincmartin 4y ago
      Yes, this is in the definition of theorems().