On 07/04/2016 02:34 PM, Heiko Becker wrote: > Hello everyone, > > > suppose I have an inductive type as follows: > > let test_IND, test_CASES = > define_type > "test = Foo num > |Bar int ";; > > Can someone explain to me how I can derive a contradiction given > equality as in the goal below? > > g `Foo 1 = Bar (&1) ==> F`;; > > Thanks in advance. > > Best regards, > > > Heiko >
Forgot to add: I want to do the proof in HOL-Light. Sorry the double post. Best regards. ------------------------------------------------------------------------------ Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San Francisco, CA to explore cutting-edge tech and listen to tech luminaries present their vision of the future. This family event has something for everyone, including kids. Get more information and register today. http://sdm.link/attshape _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
