Kevin Sullivan (Aug 02 2018 at 16:53):
Here are five lines of code:, a short version of the Hello World of Lean, suitable as a first example for even new undergraduate students. The problem pedagogically is that the result of #eval is a cryptic message about no typeclass instance, the dumping of an internal representation, and some #1s and other stuff. I understand what's going on here; the question is whether I can get Lean to show results in a readable form without defining typeclass instances. Coq's good in this regard, for example. How might I get the same effect in Lean.
| monday: day
| tuesday: day
def id_day (d: day): day := d
#eval id_day day.monday
Kenny Lau (Aug 02 2018 at 16:54):
Kevin Sullivan (Aug 02 2018 at 17:07):
Of course, thanks.
Last updated: May 08 2021 at 19:11 UTC