Skip to content

doc: improve error message for unknown attributes#14213

Open
0rca wants to merge 1 commit into
leanprover:masterfrom
0rca:av/4011-improve-error-message-1
Open

doc: improve error message for unknown attributes#14213
0rca wants to merge 1 commit into
leanprover:masterfrom
0rca:av/4011-improve-error-message-1