Skip to content
Snippets Groups Projects
Commit 41717e83 authored by Maxime Lesourd's avatar Maxime Lesourd Committed by Björn Brandenburg
Browse files

move job_cost to job.v

parent 1e4bc527
No related branches found
No related tags found
1 merge request!22Naming conventions
......@@ -3,3 +3,7 @@ From mathcomp Require Export eqtype.
(* Throughout the library we assume that jobs have decidable equality *)
Definition JobType := eqType.
(* Definition of a generic type of parameter relating jobs to a discrete cost *)
Class JobCost (J : JobType) := job_cost : J -> nat.
......@@ -22,10 +22,6 @@ Class ProcessorState (Job : eqType) (State : Type) :=
(* A schedule maps an instant to a processor state *)
Definition schedule (PState : Type) := instant -> PState.
(* Definition of a generic type of parameter relating jobs to a discrete cost *)
Class JobCost (J : JobType) := job_cost : J -> nat.
Section Schedule.
Context {Job : eqType} {PState : Type}.
Context `{ProcessorState Job PState}.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment