@avigad, could you check the following test failures? When they're fixed, I'll merge the PRs and update the web-version:
$ ./test.sh ../lean/bin/lean 04_Quantifiers_and_Equality.org
...
ERROR executing 04_Quantifiers_and_Equality.org.35.lean, for in_code_block block starting at 814, produced output:
04_Quantifiers_and_Equality.org.35.lean:12:59: error: unknown identifier 'H'
$ ./test.sh ../lean/bin/lean 11_Tactic-Style_Proofs.org
ERROR executing 11_Tactic-Style_Proofs.org.23.lean, for in_code_block block starting at 463, produced output:
11_Tactic-Style_Proofs.org.23.lean:5:16: error: invalid expression, 'by', 'begin', 'proof', 'using' or 'from' expected
11_Tactic-Style_Proofs.org.23.lean:11:3: error: invalid 'end', there is no open namespace/section
$ ./test.sh ../lean/bin/lean 13_More_Tactics.org
...
ERROR executing 13_More_Tactics.org.12.lean, for in_code_block block starting at 269, produced output:
13_More_Tactics.org.12.lean:7:0: error: tactic failed
p q : ℕ → Prop,
a b c : ℕ
⊢ p c → p b → q b → p a → (∃ (x : ℕ), p x ∧ q x)
13_More_Tactics.org.12.lean:7:0: error: failed to add declaration 'example' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
?M_1
@avigad, could you check the following test failures? When they're fixed, I'll merge the PRs and update the web-version: