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