search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Using Destruct ... eqn:.. on a hypothesis in the context #105

Closed AdamBJ closed 9 years ago

AdamBJ commented 9 years ago

I have

H5 : (if beval st b then false else true) = true

in my context and I want to destruct beval st b. If I simply do destruct (beval st b) in H5 the destruct throws away information I need (ie I'm left with true=true for one case). I remember using eqn:... to keep destruct from throwing away information, but I'm having trouble getting it to work on H5.

My attempt at a solution is destruct (beval st b) eqn:B in H5. but when I try it I get Error: b0 is used in hypothesis B.. I'm not sure where b0 is coming from, it's not in the context when I make the call to destruct. How can I make this go through?

jeehoonkang commented 9 years ago

I am quite sure destruct (beval st b) eqn:B would work.

AdamBJ commented 9 years ago

Yes, that worked. Thanks!