Module AltErgoLib.Matching_types

type gsubst = {
  1. sbs : Expr.t Var.Map.t;
  2. sty : Ty.subst;
  3. gen : int;
  4. goal : bool;
  5. s_term_orig : Expr.t list;
  6. s_lem_orig : Expr.t;
}
type trigger_info = {
  1. trigger : Expr.trigger;
  2. trigger_age : int;
  3. trigger_orig : Expr.t;
  4. trigger_formula : Expr.t;
  5. trigger_dep : Explanation.t;
  6. trigger_increm_guard : Expr.t;
}
type term_info = {
  1. term_age : int;
  2. term_from_goal : bool;
  3. term_from_formula : Expr.t option;
  4. term_from_terms : Expr.t list;
}
type info = {
  1. age : int;
  2. lem_orig : Expr.t list;
  3. t_orig : Expr.t list;
  4. but : bool;
}