Skip to Content.
Sympa Menu

ssreflect - Re: [ssreflect] NumMixin from a "\is a positive" predicate ?

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] NumMixin from a "\is a positive" predicate ?


Chronological Thread 
  • From: Pierre-Yves Strub <>
  • To:
  • Cc: Ssreflect <>
  • Subject: Re: [ssreflect] NumMixin from a "\is a positive" predicate ?
  • Date: Tue, 23 Oct 2018 12:48:51 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
  • Ironport-phdr: 9a23:I1UinhFQlcU3zRMHuTR5RZ1GYnF86YWxBRYc798ds5kLTJ78psWwAkXT6L1XgUPTWs2DsrQY07WQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDiwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE38G7VisJ+gqFVrg+/qRNj2IPUfJ2ZOeBicq/BYd8XR2xMVdtRWSxbBYO8apMCAfAAPelGtYn9vUUBoQK8CgmyGuzv0SJDiGLq3a0gzuQuChzN0Qs4H9IPrnvUts/1O7kLXeG10qnH0y7DYuhN2Tfh8ojIbwsureuKXbJtaMfcz1QkGQDdjliIt4DpIzeY2v4OvmWb9eZsSOOihmw9pw1soDWiycEhgZTTiI0P0FDL7yB5zZ41JdKmTE57ZsapEJ5KuCGbM4t6W8QiQ2B1tCojxL0KpJy2cScQxJQowB7fbPOHc4yW7R75SOmRJjJ4iGpkeLK5mRmy7VCtxvPgWsSwylpHrSpInsPRun0M1RHf8NWLR/ly80u53DaAzQHT6uVKIUAukqrbLoYswqYxlpUNq0TDBDH5lFz2ja+IaEok4fOl6//7YrX8u5+TLJV4igfjMqg2gMywHfw4MhQSX2ic4em8z6bj/VfnT7VEiv05jLXWsIzBKMQApq+5BhdV3Zw55xa+CTemytUYkmMdIFJLYhLUx7TublrfOvH8S/y4g1mquDZt3fHPeLP7UbvXKX2WqLbsZ6xwrn9CxRF79sxF+pgcXqkALejpVwrgqtHDJgQlKRG+heD6XoYunrgCUH6CV/fKeJjZtkWFs7p2cru8IbQNsTO4EMALovvnjHs3g1gYJPH7xocNdXr+GOk0ehzFM0qpuc8IFCIxhiR7VPbj0QXQSiJJenz0Wb9uvmhmWrLjNp/KQ8WWuJLE3Cq/GccINGVPC1TJFnaxMovdBKtKZyWVLcts1DcDUOr5Rg==
Hi,

> By the way the mixin factory you suggest also provides totality, maybe
> it could be cut in two bits?

That's the problem of call by need. Let's discuss this on the PR then.

Best. Pierre-Yves/

Archive powered by MHonArc 2.6.18.

Top of Page