Bug in NNG?

Stream: general

[Martin Dvořák]

I was notified about a (probably?) bug in NNG where the game says "unknown identifier add_left_cancel" instead of the message "tactic apply failed, failed to unify" which would be more helpful.
add_left_cancel.png

[Martin Dvořák]

In the best case, the game would tell the user that they attempted to use a lemma for the opposite implication, but this is not technically viable probably. However, saying "unknown identifier" when the game displays add_left_cancel as available is very confusing.

[Kevin Buzzard]

But it does unify

[Martin Dvořák]

Ah yeah!

[Kevin Buzzard]

Of course it's still worth reporting :-)

[Martin Dvořák]

In this case, the tactic should probably emit an auxilliary goal to specify n.

[Martin Dvořák]

I am not sure what the intended behavior of NNG is in such a case.

[Jon Eugster]

I created
https://github.com/leanprover-community/NNG4/issues/78

for when I'm back working -- or if somebody else has the time. It might be a problem with either the opened namespaces or the imports of that level, but should be quick to fix.