printing enumerations

Stream: general

[Thorsten Altenkirch]

I am still struggling with my type Sigma1

inductive Sigma1 : Type
| a : Sigma1
| b : Sigma1
| c : Sigma1
open Sigma1

I now learnt how to derive fintype, but I also would like to print it. Actually I would like to print:

def w : word Sigma1 := [a,b]
def v : word Sigma1 := [b,c]
#eval (w++v)

because I don't like

(#1 #0 (#1 #1 (#1 #1 (#1 #2 #0))))

so I tried to say:

@[derive fintype,derive has_repr]
inductive Sigma1 : Type
| a : Sigma1
| b : Sigma1
| c : Sigma1
open Sigma1

but this doesn't work. It seems to know how to print lists of printable things though.

[Chris Hughes]

This should work, but I'm not sure because the computer I'm at right now doesn't have Lean. Maybe there's a better way with a derive but I don't know it.

instance : has_repr Sigma1 :=
  ⟨λ s,
    match s with
    | Sigma1.a := "a"
    | Sigma1.b := "b"
    | Sigma1.c := "c"
    end⟩

[Thorsten Altenkirch]

Thank you - this is helpful. But I was hoping for an automatic method.

[Adam Topaz]

I can't seem to get it to derive the fintype instance. What are your imports?

[Chris Hughes]

tactic.derive_fintype maybe?

[Kevin Buzzard]

import tactic worked for me in the other thread

[Eric Wieser]

Thorsten Altenkirch said:

Thank you - this is helpful. But I was hoping for an automatic method.

Sounds like a great excuse to learn to write metaprograms :)

[Kevin Buzzard]

I would discourage learning how to write metaprograms in lean 3 though because the story is different in lean 4 and migration is happening

[Thorsten Altenkirch]

Kevin Buzzard said:

I would discourage learning how to write metaprograms in lean 3 though because the story is different in lean 4 and migration is happening

Is there any advice how to write this metaprogram in lean4? It should actually work for any algebraic datatype (no constructors with function arguments).

[Reid Barton]

In Lean 4 deriving Repr works already, sorry :smile:

[Thorsten Altenkirch]

How can I put my toes in the lean4 water but I am still able to revert to lean3 if I don't like it?

[Mario Carneiro]

the lean 4 and lean 3 extensions coexist, the lean-toolchain file determines which one your project is

[Kevin Buzzard]

The only reason I made the comment was that the type theories of Lean 3 and Lean 4 are identical, but the metaprogramming set-ups are completely different, so whilst learning Lean's type theory via Lean 3 is a great idea, learning how to write tactics in Lean 3 is a dead end now.