Module Qcert.Data.Model.ForeignData

Require Import EquivDec.
Require Import CoqLibAdd.

Section ForeignData.
  
  Class foreign_data : Type
    := mk_foreign_data {
           foreign_data_model : Set
           ; foreign_data_dec :> EqDec foreign_data_model eq
           ; foreign_data_normalized (a : foreign_data_model) : Prop
           ; foreign_data_normalize (a : foreign_data_model) : foreign_data_model
           ; foreign_data_normalize_normalizes (a : foreign_data_model) : foreign_data_normalized (foreign_data_normalize a)
           ; foreign_data_normalize_idempotent (a : foreign_data_model) : foreign_data_normalized a -> foreign_data_normalize a = a
           ; foreign_data_tostring :> ToString foreign_data_model
      }.

End ForeignData.