CALL FOR PARTICIPATION
The 7th ACM SIGPLAN International Conference
on Certified Programs and Proofs (CPP 2018)
co-located with POPL 2018
in cooperation with ACM SIGLOG
http://conf.researchr.org/track/CPP-2018/CPP-2018
8-9 January, 2018,
Call for Papers
WiL 2018: Second Women in Logic Workshop
Oxford, UK
July 8, 2018
https://sites.google.com/site/womeninlogic2018/welcome/
Affiliated with the Thirty-Third Annual ACM/IEEE Symposium on Logic
-- Apologies for multiple postings --
STAF 2018: Software Technologies: Applications and Foundations
June 25-29, 2018, Toulouse, France
Web: http://www.staf2018.fr
Call for Workshops
That's to say, I need to create my own sorted predicate? I realised it in the
past few days, however, I have no idea about this, I always wanted to implement
it by myself. But now, I find I just need to use SORTED,as follows:
val mysorted_def = Define `
mysorted xs = SORTED (\x y. x <= y)
