List of expressions to expression for that list

Stream: Is there code for X?

[Eric Wieser]

Do we have anything like this?

meta def list.to_pexpr : list pexpr → pexpr
| [] := ``([])
| (x :: xs) := ``(list.cons %%x %%xs.to_pexpr)

-- list.cons 1 (list.cons 2 list.nil)
#eval tactic.trace ([``(1), ``(2)].to_pexpr)

[Damiano Testa]

If I understand correctly, you can also define your function as follows, right?

meta def list.to_pexpr (lp : list pexpr) : pexpr :=
(lp.drop 1).foldl (λ e f : pexpr, ``(list.cons %%e %%f)) ((lp.nth 0).get_or_else ``([]))

Even if this is the case, I am not sure this is better...

[Damiano Testa]

With my version, I get

#eval tactic.trace ([``(1), ``(2)].to_pexpr)
-- list.cons 1 2

that maybe suggests that what I proposed is not what you want...

[Eric Wieser]

list.cons 1 2 is nonsense because 2 is not a list

[Damiano Testa]

Is this better?

meta def list.to_pexpr1 (lp : list pexpr) : pexpr :=
lp.foldr (λ e f, ``(list.cons %%e %%f)) ``([])

[Eric Wieser]

yes, that means the same as what I wrote, but it doesn't answer the question of whether such a construct already exists

[Damiano Testa]

I could not find it, but, given the explanations that I needed to understand what the issue was, this is probably not an interesting data point... :face_palm:

[Eric Wieser]

Perhaps this would be a reasonable sort of thing to use docs#has_to_pexpr for