Qcert.Basic.TypeSystem.DType

Section DType.



  Context {ftype:foreign_type}.
  Context {br:brand_relation}.

  Inductive drtype : Set :=
  | Tlocal : rtype → drtype
  | Tdistr : rtype → drtype.

  Global Instance drtype_eqdec : EqDec drtype eq.

  Section unlocalize.
    Definition unlocalize_drtype (dt:drtype) : rtype :=
      match dt with
      | Tlocal t ⇒ t
      | Tdistr t ⇒ Coll t
      end.

  End unlocalize.

End DType.