- [ MEM_FUNC ⇒ λm:aux_mem_type MEM_FUNC.
- λc:aux_chk_type MEM_FUNC.
- λaddr:word16.
- λv:byte8.
- mf_mem_update m c addr v
- | MEM_TREE ⇒ λm:aux_mem_type MEM_TREE.
- λc:aux_chk_type MEM_TREE.
- λaddr:word16.
- λv:byte8.
- mt_mem_update m c addr v
- | MEM_BITS ⇒ λm:aux_mem_type MEM_BITS.
- λc:aux_chk_type MEM_BITS.
- λaddr:word16.
- λv:byte8.
- mb_mem_update m c addr v
- ].
+ [ MEM_FUNC ⇒ mf_mem_update
+ | MEM_TREE ⇒ mt_mem_update
+ | MEM_BITS ⇒ mb_mem_update
+ ] m (chk_get t c addr) addr v.