[#15020] fix: remove lossy syntax separator array coercions - #44
Open
downstream-lean4[bot] wants to merge 1 commit into
Open
[#15020] fix: remove lossy syntax separator array coercions#44downstream-lean4[bot] wants to merge 1 commit into
downstream-lean4[bot] wants to merge 1 commit into