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
------------------------------------------------------------------------------
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
