Qcert.Basic.Data.ForeignData

Section ForeignData.



  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.