AltErgoLib.Matching_types
type gsubst = {
sbs : Expr.t Symbols.Map.t; |
sty : Ty.subst; |
gen : int; |
goal : bool; |
s_term_orig : Expr.t list; |
s_lem_orig : Expr.t; |
}
type trigger_info = {
trigger : Expr.trigger; |
trigger_age : int; |
trigger_orig : Expr.t; |
trigger_formula : Expr.t; |
trigger_dep : Explanation.t; |
}