leanprover / theorem_proving_in_lean

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

nat seems to be 'imported' automatically #69

Closed holtzermann17 closed 5 years ago

holtzermann17 commented 5 years ago

The file says:

If we import ``nat``, we can use ``weekday.rec_on`` to define a function from ``weekday`` to the natural numbers:

But the sample code doesn't actually import nat, and it works fine.