kdrag.datatype.inj_lemmas

kdrag.datatype.inj_lemmas(dt: DatatypeSortRef) → list[Proof]

Injectivity lemmas for a datatype. Z3 internally understands these, but can be useful to be explicit about them in some situations

>>> import kdrag.theories.nat as nat
>>> inj_lemmas(nat.Nat)[0]
|= ForAll([x!..., y!...],
       (S(x!...) == S(y!...)) == And(x!... == y!...))