pedagogy vs. "dumping internal representation"

Stream: general

[Kevin Sullivan]

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.

inductive day
| monday: day
| tuesday: day

def id_day (d: day): day := d

#eval id_day day.monday

[Kenny Lau]

#reduce

[Kevin Sullivan]

#reduce

Of course, thanks.