Module ForeignData

Section ForeignData.

  Require Import EquivDec.

  Require Import RUtil.
  
  Class foreign_data : Type
    := mk_foreign_data {
           foreign_data_type : Set
           ; foreign_data_dec :> EqDec foreign_data_type eq
           ; foreign_data_normalized (a : foreign_data_type) : Prop
           ; foreign_data_normalize (a : foreign_data_type) : foreign_data_type
           ; foreign_data_normalize_normalizes (a : foreign_data_type) : foreign_data_normalized (foreign_data_normalize a)
           ; foreign_data_normalize_idempotent (a : foreign_data_type) : foreign_data_normalized a -> foreign_data_normalize a = a
           ; foreign_data_tostring :> ToString foreign_data_type
      }.

End ForeignData.