Hi Ramana, >Apparently Coq somewhat recently gained the ability to be explicit about >proof structure: >http://poleiro.info/posts/2013-06-27-structuring-proofs-with-bullets.html >(Of course that comes naturally when using tacticals like THEN, THEN1, etc.)
Not _very_ recently. It was introduced in 8.4, which is from late 2011. And maybe Ssreflect had it long before that already? (In my opinion Ssreflect is a much underrated proof language, even if it looks like perl.) Of course in Flyspeck many (most?) proofs are the other way around, where there is just a list of tactics that is processed like you would successively "e" them interactively. I think Mark Adams tactician is exactly about converting a THEN-THEN proof to that format? But I agree that a more structured "bulleted" proof is nicer. Even though ergonomically of course having to type THEN is monstrous. Freek ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
