Skip to content
Snippets Groups Projects
Commit acc353bd authored by Kimaya Bedarkar's avatar Kimaya Bedarkar Committed by Björn Brandenburg
Browse files

addition to basic facts

parent 0727d647
No related branches found
No related tags found
1 merge request!168addition to basic facts
Pipeline #56309 passed with warnings
Stage: build
    Stage: process
      Hide whitespace changes
      Inline Side-by-side
      analysis/facts/behavior/arrivals.v
      + 6
      − 3
      View file @ acc353bd
      ......@@ -118,9 +118,12 @@ Section Arrived.
      End Arrived.
      (** We add the above lemma into a "Hint Database" basic_facts, so Coq
      will be able to apply it automatically. *)
      Global Hint Resolve valid_schedule_implies_jobs_must_arrive_to_execute : basic_facts.
      (** We add some of the above lemmas to the "Hint Database"
      [basic_facts], so the [auto] tactic will be able to use them. *)
      Global Hint Resolve
      valid_schedule_implies_jobs_must_arrive_to_execute
      jobs_must_arrive_to_be_ready
      : basic_facts.
      (** In this section, we establish useful facts about arrival sequence prefixes. *)
      Section ArrivalSequencePrefix.
      ......
      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