Commit 7507d62e authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files

Fix comment

parent 7755715d
......@@ -46,8 +46,8 @@ Module ArrivalSequence.
Definition job_arrival {arr_seq: arrival_sequence Job} (j: JobIn arr_seq) :=
_arrival_time arr_seq j.
(* Finally, we assume a decidable equality for JobIn. We don't care about
its definition. It's just to make JobIn compatible with ssreflect. *)
(* Finally, we assume a decidable equality for JobIn, to make it compatible
with ssreflect. TODO: Is there a better way to do this? *)
Definition jobin_eqdef (arr_seq: arrival_sequence Job) :=
(fun j1 j2: JobIn arr_seq => (JobIn_is_Job j1) == (JobIn_is_Job j2)).
Axiom eqn_jobin : forall arr_seq, Equality.axiom (jobin_eqdef arr_seq).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment