RuleAntiunification (astral.Astral_internal.RuleAntiunification)

module Logger : Logger_sig.LOGGER

module Substition : sig ... end

val anti_unify_term : 
  SL.Term.t ->
  SL.Term.t ->
  SL.Term.t list SL.Variable.Map.t

Antiunify two terms of the same sort.

val anti_unify_terms : 
  SL.Term.t list ->
  SL.Term.t list ->
  SL.Term.t list SL.Variable.Map.t option

val anti_unify : SL.t -> SL.t -> SL.Term.t list SL.Variable.Map.t option

val apply_pair : SL.t -> SL.t -> SL.t list

val apply : InductiveDefinition.t -> InductiveDefinition.t