chore: use String.ofList instead of String.mk in elaborator+kernel
#14477
Loading
String.ofList instead of String.mk in elaborator+kernel
#14477