In addition to introducing primitives Map_Pack and Map_Unpack, this PR also adds assumptions about well-formed maps to IS checkers (base, step, conclusion). Other checkers introduced by ISR remain. These assumptions should be added once the dust has settled on the implementation of ISR.
In addition to introducing primitives Map_Pack and Map_Unpack, this PR also adds assumptions about well-formed maps to IS checkers (base, step, conclusion). Other checkers introduced by ISR remain. These assumptions should be added once the dust has settled on the implementation of ISR.
cc: @NamrathaG