search

project-everest / mitls-fstar

Verified implementation of TLS 1.3 in F*
https://www.mitls.org
Other
173 stars 16 forks source link

List.Helpers: improve a spec #245

Closed mtzguido closed 4 years ago

mtzguido commented 4 years ago

No need to use FStar.List.Tot.mem_filter_spec which is only meaningful for eqtypes. This will also be removed from F* by the following PR https://github.com/FStarLang/FStar/pull/2105.