Ignore:
Timestamp:
Feb 2, 2011, 12:41:05 PM (9 years ago)
Author:
campbell
Message:

Fix treatment of pointers in initialisation data, a little like later versions
of CompCert?. Remove obsolete Init_pointer.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Errors.ma

    r250 r485  
    1717include "Plogic/equality.ma".
    1818include "Plogic/connectives.ma".
     19include "datatypes/sums.ma".
    1920
    2021(* * Error reporting and the error monad. *)
     
    192193  end.
    193194*)
     195
     196
     197ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].
     198nlemma opt_OK: ∀A,P,e.
     199  (∀v. e = Some ? v → P v) →
     200  match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ].
     201#A P e; nelim e; /2/;
     202nqed.
Note: See TracChangeset for help on using the changeset viewer.