Hi Haitao, it all depends on what exactly you want to do. Sometimes it is as easy as using GSYM instead of SYM. Of you can use something like DEPTH_CONV or ONCE_DEPTH_CONV. That's how GSYM is defined in terms of SYM. Or you could use something more specialised like STRIP_BINDER_CONV or STRIP_QUANT_CONV. Notice that these are all conversionen, so you wrap the whole thing in CONV_RULE.
Best Thomas On 28.02.19 09:38, Haitao Zhang wrote: > Rules like SYM do not work with top level binders. What is the > recommended way to use them with binders without having to stack up > SPEC and GEN? > > Thanks, > Haitao > > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
