Module Annot.IAnnot

type res = (Rid.t * Mlsem_types.Ty.t) option
type coverage = res * Mlsem_common.REnv.t
type branch =
  1. | BMaybe of t
  2. | BType of t
  3. | BSkip
and inter_branch = {
  1. coverage : coverage option;
  2. ann : t;
}
and inter = inter_branch list
and part = (Mlsem_types.Ty.t * LazyIAnnot.t option) list
and a =
  1. | Untyp
  2. | AVar of Mlsem_types.MVarSet.t -> Mlsem_types.Subst.t
  3. | AConstruct of t list
  4. | ALet of t * part
  5. | AApp of t * t * Mlsem_types.Ty.t
  6. | AOp of Mlsem_types.MVarSet.t -> Mlsem_types.Subst.t * t * Mlsem_types.Ty.t
  7. | AProj of t * Mlsem_types.Ty.t
  8. | ACast of Mlsem_types.GTy.t * t
  9. | ACoerce of Mlsem_types.GTy.t * t
  10. | AIte of t * Mlsem_types.GTy.t * branch * branch
  11. | ALambda of Mlsem_types.GTy.t * t
  12. | ALambdaRec of (Mlsem_types.GTy.t * t) list
  13. | AAlt of t option * t option
  14. | AInter of inter
and t =
  1. | A of Annot.t
  2. | I of {
    1. rid : Rid.t;
    2. ann : a;
    3. refinement : Mlsem_common.REnv.t;
    }
val substitute : Mlsem_types.Subst.t -> t -> t
val pp : Stdlib.Format.formatter -> t -> unit
val pp_a : Stdlib.Format.formatter -> a -> unit
val pp_coverage : Stdlib.Format.formatter -> coverage -> unit
val pp_res : Stdlib.Format.formatter -> res -> unit