search

JetBrains / Arend

The Arend Proof Assistant
https://arend-lang.github.io/
Apache License 2.0
689 stars 33 forks source link

Be kinder to goals in more places #226

Open ice1000 opened 4 years ago

ice1000 commented 4 years ago

Right now we produce errors for goals in some contexts:

image image image image

Maybe we can produce goal warnings instead.

valis commented 4 years ago

In the last two examples, that's impossible because after '\extends' it expects a name and not an arbitrary expression. And what's the point of putting a goal there anyway?

ice1000 commented 4 years ago

We can don't support those cases. I agree that it's kinda pointless to put a goal there