Function mk_eq

examples/05_knuckledragger/python/main.py:53–60

(lhs, rhs)

        return Expr.app(Expr.app(op, a), b)

    def mk_eq(lhs, rhs):
        return Expr.app(
            Expr.app(
                Expr.app(mk_const("Eq"), mk_const("Nat")),
                lhs,
            ),
            rhs,
        )


    print("== expr_to_z3 ==")