data specification
using buffer
data types leb := unmapped
| erased
| mapped(. .data : buffer;. .fill : nat) with .mapped?
;
variables leb : leb;
end data specification