kdrag.theories.int
Builtin theory of integers
Module Attributes
@kd.PTheorem( |
Functions
|
|
|
- kdrag.theories.int.induct_nat(x, P)
- kdrag.theories.int.induct_nat_strong(x, P)
- kdrag.theories.int.natpair_to_tuple = natpair_to_tuple
- @kd.PTheorem(
- ForAll(
[n, m], n >= 0, m >= 0, And(
natpair_to_tuple(natpair(n, m))[0] == n, natpair_to_tuple(natpair(n, m))[1] == m,
),
)
) def unpair_natpair(l):
n, m = l.fixes() l.generalize(n) # TODO: should remove from context m = l.induct(m) # n = l.fix() # _n = l.induct(n) # l.auto() # l.auto(by=[natpair.defn, natpair_to_tuple.defn])
# n = l.induct(n) # l.auto(by=[natpair.defn, natpair_to_tuple.defn]) # l.auto(by=[natpair.defn, natpair_to_tuple.defn])
# l.auto(by=[natpair.defn, natpair_to_tuple.defn])
# l.auto(by=[natpair.defn, natpair_to_tuple.defn])