Zulip Chat Archive

Stream: general

Topic: pedagogy vs. "dumping internal representation"


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.

inductive day
| monday: day
| tuesday: day

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

#eval id_day day.monday

Kenny Lau (Aug 02 2018 at 16:54):

#reduce

Kevin Sullivan (Aug 02 2018 at 17:07):

#reduce

Of course, thanks.


Last updated: Dec 20 2023 at 11:08 UTC