Qcert.Compiler.QLib.QUtil

Module QUtil(runtime:CompilerRuntime).


  Definition mr_reduce_empty := mr_reduce_empty.

  Definition type_annotation {br:brand_relation} (A:Set): Set
    := TDNNRCInfer.type_annotation A.

  Definition ta_base {br:brand_relation} (A:Set) (ta:type_annotation A)
    := TDNNRCInfer.ta_base ta.
  Definition ta_inferred {br:brand_relation} (A:Set) (ta:type_annotation A)
    := TDNNRCInfer.ta_inferred ta .
  Definition ta_required {br:brand_relation} (A:Set) (ta:type_annotation A)
    := TDNNRCInfer.ta_required ta.

  Definition validate_lifted_success := validate_lifted_success.

  Definition mkDistLoc := mkConstants mkDistLoc.   Definition mkDistWorld env := mkConstants (mkDistWorld env). End QUtil.