coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?

From: Michiel Helvensteijn <mhelvens AT gmail.com>
To: Hendrik Tews <tews AT os.inf.tu-dresden.de>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?
Date: Tue, 16 Jul 2013 13:08:32 +0200

On Tue, Jul 16, 2013 at 12:21 PM, Hendrik Tews
<tews AT os.inf.tu-dresden.de>
wrote:

> For the comparison of sumor vs. precondition, I would say that in
> proofs, sumor does _always_ cause a little bit of trouble, while
> the precondition may cause big trouble sometimes.
>
> <...>

Thanks! You do make the sumor idiom seem very attractive. :-)

--
www.mhelvens.net

[Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Pierre-Marie Pédrot, 07/14/2013
  - Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Michiel Helvensteijn, 07/14/2013
    - Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Arnaud Spiwack, 07/15/2013
      - Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Michiel Helvensteijn, 07/16/2013
        
        Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Arnaud Spiwack, 07/16/2013
        
        Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Michiel Helvensteijn, 07/16/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Hendrik Tews, 07/16/2013
  - Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Michiel Helvensteijn, 07/16/2013
    - Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Hendrik Tews, 07/17/2013
      - Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Michiel Helvensteijn, 07/17/2013