ssreflect - Re: [ssreflect] ListSet in ssreflect

Subject: Ssreflect Users Discussion List

List archive

From: Felipe Cerqueira <>
To:
Subject: Re: [ssreflect] ListSet in ssreflect
Date: Thu, 21 Apr 2016 15:02:27 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=Pass ; spf=None
Ironport-phdr: 9a23:imAGyB2bSZL54SHOsmDT+DRfVm0co7zxezQtwd8ZsegTKPad9pjvdHbS+e9qxAeQG96Lu7Qa26GP6/yocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC34Lph6vro8GbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBL7hZak2SbFTEBwjKHpw5cvxtBCFTA2V53JaXH9FvABPBl3r4RX7Rpq5mSbgr/dw2TOTdZn4QLQ1QTmpx6JzSVrzlzxBMCQ2pjKEwvdshb5W9Ury7yd0xJTZNdmY

On 4/21/16 2:52 PM, Laurent Thery wrote:

Canonical mem_set_predType T := mkPredType (fun (l : set T) => mem_seq (_set_seq l)).

Yes, thanks! I tried this now and it's working:

Variable s: {set nat}.
Check (10 \in (map (fun x => 2*x) s)).

[ssreflect] Bijection between subsets, Florent Hivert, 04/21/2016
- RE: [ssreflect] Bijection between subsets, Georges Gonthier, 04/21/2016
  - [ssreflect] ListSet in ssreflect, Felipe Cerqueira, 04/21/2016
    - Re: [ssreflect] ListSet in ssreflect, Laurent Thery, 04/21/2016
      - Re: [ssreflect] ListSet in ssreflect, Felipe Cerqueira, 04/21/2016
        
        Re: [ssreflect] ListSet in ssreflect, Laurent Thery, 04/21/2016
        
        Re: [ssreflect] ListSet in ssreflect, Felipe Cerqueira, 04/21/2016
    - Re: [ssreflect] ListSet in ssreflect, Cyril, 04/21/2016
      - Re: [ssreflect] ListSet in ssreflect, Christian Doczkal, 04/21/2016
        
        Re: [ssreflect] ListSet in ssreflect, Felipe Cerqueira, 04/21/2016