1. 15 Apr, 2021 1 commit
  2. 15 Mar, 2021 3 commits
  3. 12 Mar, 2021 3 commits
    • Edoardo Putti's avatar
      add the trivial hoare triple rules · d1ce44c2
      Edoardo Putti authored
      d1ce44c2
    • Edoardo Putti's avatar
      refactor proof rules and use them to prove examples · 27638c50
      Edoardo Putti authored
      the proof rules definitions were ok but to actually use
      them effectively and have the eauto or eapply instance the correct
      parts for us we have to refactor them so that we can specify the
      interesting parts of our goals ourself and have eauto pick up for us
      
      As an example in the context proof rule reordering from
      
      Lemma hoare_ctxS E P P' e Q v
      
      to
      
      Lemma hoare_ctxS E P' P e Q v
      
      makes it possible for us to specify both the context we want
      to use and the intermediate heap P' while having eauto fill out
      P e Q v for us
      27638c50
    • Edoardo Putti's avatar
      prove alloc rule · c99f9661
      Edoardo Putti authored
      c99f9661
  4. 08 Mar, 2021 5 commits
  5. 04 Mar, 2021 8 commits
  6. 03 Mar, 2021 17 commits
  7. 01 Mar, 2021 3 commits