Mathlib4 Parsing Error #122

New Issue

aniva · 2024-11-15T23:11:50-08:00

aniva commented

2024-11-15 23:11:50 -08:00

https://github.com/lenianiva/PyPantograph/issues/44

  File "<...>/PyPantograph/pantograph/server.py", line 244, in tactic_invocations
    raise ServerError(result["desc"])
pantograph.server.ServerError: unknown constant 'term.pseudo.antiquot'

The error occurs when parsing Mathlib/ModelTheory/Syntax.lean

https://github.com/lenianiva/PyPantograph/issues/44 ``` File "<...>/PyPantograph/pantograph/server.py", line 244, in tactic_invocations raise ServerError(result["desc"]) pantograph.server.ServerError: unknown constant 'term.pseudo.antiquot' ``` The error occurs when parsing `Mathlib/ModelTheory/Syntax.lean`

aniva added this to the 0.3 milestone 2024-11-15 23:11:50 -08:00

aniva added the

labels 2024-11-15 23:11:50 -08:00

aniva self-assigned this 2024-11-15 23:11:50 -08:00

aniva modified the milestone from 0.3 to 0.2.22

2024-12-06 00:09:29 -08:00

aniva referenced a pull request that will close this issue