ReduceEval and String

Stream: lean4

[Alex Keizer]

I am writing some meta-code where I want to turn an Expr describing a String into an actual String object.
I initially thought reduceEval was what I want, but it seems to only work for string literals:

import Qq
open Qq Lean.Meta

#eval (reduceEval q("a") : MetaM String) -- "a"

/- reduceEval: failed to evaluate argument
    "a" ++ "b" -/
#eval (reduceEval q("a" ++ "b") : MetaM String)

Is this by design or a bug?

[Alex J. Best]

I don't know about reduceEval but you can do

#eval (evalExpr String q(String) q("a" ++ "b") : MetaM String)

[Alex Keizer]

Thanks! That indeed works for my minimized example, but for my actual code evalExpr throws an incomplete case error

[Alex J. Best]

What is in your actual code that causes that?