Zulip Chat Archive

Stream: new members

Topic: infoview is a unique feature

Huỳnh Trần Khanh (Jun 14 2021 at 16:39):

is infoview a unique feature of lean? does this feature exist in other theorem proving languages?

Huỳnh Trần Khanh (Jun 14 2021 at 16:41):

i'm browsing an isabelle/hol proof right now and there is no infoview :cry:

Patrick Massot (Jun 14 2021 at 17:29):

Of course it exists everywhere. Otherwise the software isn't called an interactive theorem prover.

Jason Rute (Jun 14 2021 at 18:10):

But, some theorem provers, like HOL Light for one example, do the interactive part very differently. I guess the question is what is it about the info view that you are asking about?

Huỳnh Trần Khanh (Jun 15 2021 at 00:13):

so... I know this is somewhat off topic but where is the infoview in Isabelle/HOL :joy:

Last updated: Dec 20 2023 at 11:08 UTC