search

imandra-ai / imandra-vscode

VSCode extension for developing imandra
Other
2 stars 0 forks source link

Support `lemma` on equal footing with `theorem` #5

Closed grantpassmore closed 6 years ago

grantpassmore commented 6 years ago

Currently, it seems lemma isn't treated on equal footing with theorem, let, type, verify, etc. It should be.

image

c-cube commented 6 years ago

I think it's the same for the "instance" keyword.

ewenmaclean commented 6 years ago

do we want the same behaviour for the instance keyword? Could you let me know all the keywords that I should know about and their grouped patterns?

I have fixed this for lemma but will not release right now as there will be a problem (annotated in README) with updating the package version.

grantpassmore commented 6 years ago

Yes, should be the same for instance. These should all be on equal footing:

let, type, theorem, verify, lemma, instance

grantpassmore commented 6 years ago

Closed by https://github.com/AestheticIntegration/imandra-vscode/commit/6c210211d87434fae2185698c819031231f9eafc

grantpassmore commented 6 years ago

Reopening as it seems we don't yet support instance

grantpassmore commented 6 years ago

instance is supported! Closing