← Copula mathematical handbook

Homomorphism rules for ISize used by the grind tactic. The injection function is ISize.toBitVec.

theorem Lean.Grind.ISize.toInt_eq_toBitVec_toInt (x : ISize) : x.toInt = x.toBitVec.toInt

Translations of ≤ and < into the target domain.