The definition of service_at in ideal.v service_on in ideal.v is given using the implicit conversion nat_of_bool as s == Some j.
service_at
service_on
nat_of_bool
s == Some j
Unfolding this definition would give if s == Some j then 1 else 0 which should be equivalent and feels more readable.
if s == Some j then 1 else 0
changed the description
mentioned in commit 42008f41
mentioned in merge request !199 (merged)
assigned to @bbb
closed with commit 42008f41