-(* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
-nlet rec mf_load_from_source_at (old_mem:word16 → byte8) (source:list byte8) (addr:word16) on source ≝
-match source with
- (* fine di source: carica da old_mem *)
- [ nil ⇒ old_mem
- | cons hd tl ⇒ λx:word16.match lt_w16 x addr with
- (* e' prima di source: carica da old_mem *)
- [ true ⇒ old_mem x
- | false ⇒ match eq_w16 x addr with
+(* carica a paratire da addr, overflow se si supera 0xFFFF... *)
+nlet rec mf_load_from_source_at (old_mem:word16 → byte8) (src:list byte8) (addr:word16) on src ≝
+ match src with
+ (* fine di source: carica da old_mem *)
+ [ nil ⇒ old_mem
+ | cons hd tl ⇒ λx:word16.match eq_w16 addr x with