kdrag.kernel.ext

kdrag.kernel.ext(domain: Sequence[SortRef], range_: SortRef) → Proof

>>> ext([smt.IntSort()], smt.IntSort())
|= ForAll([f, g], (f == g) == (ForAll(x0, f[x0] == g[x0])))
>>> ext([smt.IntSort(), smt.RealSort()], smt.IntSort())
|= ForAll([f, g],
       (f == g) ==
       (ForAll([x0, x1],
               Select(f, x0, x1) == Select(g, x0, x1))))

Parameters:

• domain (Sequence[SortRef])

• range_ (SortRef)

Return type:

Proof