The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

>     We frequently have goals where "P" is large. Usually that's an accident
>     ;-)  but for example, proving a Hoare triple about an interesting piece
>     of code can result in a pretty long goal of which only the beginning
>     (the expression in head position) is interesting.
> 
> 
> You are of the "strongest postcondition" chapel then. And Thou shall
> Burn in Hell for such perverted practice! :-)

Actually, we're using weakest preconditions. ;)

> Then telescope being yet another set of hypothesis (cf R. Krebbers proof 
> mode), they would go in yet another window?
> 
> Leading to something like:
> 
> 
> H1:...  scrollable
> H2: ..
> ================
> P1
> P2     scrollable
> P3
> ----------------
> P    scrollable
> 

Right, the Hoare triple I talked about is just the conclusion in
Robbert's proof mode. So I guess PG has little chance of understanding
that goal anyway.

Doesn't putting all these things into separate buffers waste enormous
amounts of space, i.e. those extra status lines and scrollbars emacs
puts at the bottom of a buffer?

Kind regards,
Ralf