[Hol-info] question about LET expanding

[Michael N. <Mic...@ni...>]

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.