Skip to content

Definition of service for ideal schedules

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.

Unfolding this definition would give if s == Some j then 1 else 0 which should be equivalent and feels more readable.

Edited by Björn Brandenburg