Michel Demazure comments

Repositories
Issues
Comments

Results 2 comments of


                                            Michel Demazure

Allow return value contract to reference input contract?

And what about a contract on values like the one for division: (a, b) -> (q,r), with contract a == bq+r ?

Allow return value contract to reference input contract?

@egonSchiele, @nixpulvis : Yes, exactly to the point. Dependent types are what I thought of (I am familiar with them, in proof assistants, like Coq). It would wonderful - and...