search

leanprover / theorem_proving_in_lean

Theorem proving in Lean
Apache License 2.0
47 stars 47 forks source link

follow directions to avoid conflicts #70

Closed holtzermann17 closed 5 years ago

holtzermann17 commented 5 years ago

The text says

To run these examples, we put them in a namespace called hidden, so that a name like bool does not conflict with the bool in the standard library.

I've just adjusted the code so that the namespace instructions appear in the HTML export.