fact: Definition match_address (spec: address_spec) (addr: address) : bool := match spec.(smask) with | Some mask => N.eqb (N.land addr mask) (N.land spec.(saddr) mask) | None => N.eqb addr spec.(saddr) end.
imports: Coq.Lists.List Fiat.Narcissus.Examples.Guard.Core