search

metamath / metamath-exe

Metamath program - source code for the Metamath executable
GNU General Public License v2.0
75 stars 25 forks source link

Check tokens in math strings embedded in comments #159

Open tirix opened 11 months ago

tirix commented 11 months ago

Discussion in the PR set.mm#3323 showed that metamath-exe did not verify that each symbol in a math string embedded in comments (within `) is actually a valid math symbol.

This check could be added in metamath-exe.