[Hol-info] Experience and opinions on proof assistants with “rich” type systems

Hello. I want ask for your experience and opinion of proof assistants with “rich” type systems (allowing types dependent on terms and “proofs as terms, propositions as types”) like Agda and Coq. Specifically, how practical are these systems for pure mathematics, compared to HOL4 and HOL Light? Is

[Hol-info] A small question about Datatype.

Hi, I have a small question about Datatype. I define a type coordinate as follow: Datatype `coordinate = <| x_axis: real; y_axis: real; z_axis: real |>`; it derived and stored some relevant theorems, like coordinate_component_equality, now I want to use this theorem, I

[Hol-info] [fm-announcements] NASA Formal Methods Symposium 2018 - CFP

NFM 2018 - Call for Papers The 10th NASA Formal Methods Symposium 30 Years of Formal Methods at NASA - https://shemesh.larc.nasa.gov/NFM2018/ April 17-19, 2018 Newport News Marriott at City Center Newport News, VA, USA Theme of the Symposium