[Hol-info] Federated Logic Conference student travel support

Friends, As program committee co-chairs of Interactive Theorem Proving 2018, we would like to share the information below. We have also added it to the ITP web pages: https://itp2018.inria.fr/venue/ The FLoC web pages are here: http://www.floc2018.org/ Best wishes, Jeremy Avigad and Assia

[Hol-info] SAT/SMT/AR Summer School 2018

[Apologise for cross-posting. Please forward to anybody you think may be interested] SAT/SMT/AR Summer School 2018 University of Manchester, 3-6th July http://ssa-school-2018.cs.manchester.ac.uk

[Hol-info] Question about Type (:M+N) in HOL Light

Hi, everyone. I know the type :(M,N)finite_sum in library "Definition of finite Cartesian product types". What is the difference between (:M+N) and :(M,N)finite_sum? Is there the theorem |- dimindex (:M+N) = dimindex(:M)+dimindex(:N) in the existing library? Thank you very much. Best regard