clutch.eris.eris

From stdpp Require Import namespaces.
From clutch.prob_lang Require Export notation tactics metatheory.
From clutch.prob_lang Require Export lang.
From clutch.eris Require Export lifting ectx_lifting primitive_laws derived_laws
  total_primitive_laws total_derived_laws proofmode error_rules presample_rules.