

def substitute(t, subs):
    '\n    Return the term obtained from t by simultaneous substitution given\n    by subs\n\n    subs is either a dictionary or a mapping given by an iterable of\n    (key, value) pairs\n\n    Both keys and values in subs can be either Var or Const.\n    All keys in subs will be substituted by their values in subs.\n\n    For variables, only free occurances will be substituted.\n\n    If the substitution will create capturing of a free variable, the\n    substitution will fail with an error.\n    '
    if (not isinstance(subs, dict)):
        subs = dict(subs)
    if (type(t) in (Var, Const)):
        if (t in subs):
            return subs[t]
        else:
            return t
    elif (type(t) in (Apply, Eq, Ite, Not, And, Or, Implies, Iff)):
        return type(t)(*(substitute(x, subs) for x in t))
    elif (type(t) in (ForAll, Exists)):
        forbidden_variables = free_variables(*subs.values())
        if forbidden_variables.isdisjoint(t.variables):
            return type(t)(t.variables, substitute(t.body, ((k, v) for (k, v) in subs.iteritems() if (k not in t.variables))))
        else:
            assert False, (t, k)
    else:
        assert False, type(e)

dataset/ETHPy150Open Microsoft/ivy/ivy/logic_util.py substitute/VarMisuse@224/449 `subs`->`k`