|
From: Michael N. <Mic...@ni...> - 2006-04-15 09:42:23
|
Kenro Yatake writes: > I have a question about tactics. > ------------------------ > Are there any built-in tactics to expand the following kind of LET terms > with pairs? > g `let (a,b) = c in a + b = x`: > -> g `FST c + SND c = x` Assuming you are using Kananaskis-3, you can use bossLib.RW_TAC or bossLib.SRW_TAC to perform this sort of transformation. In fact, those tactics handle let-expressions specially - possibly introducing abbreviation assumptions. Michael. |