Function canonical_int 

pub fn canonical_int(n: i64) -> Term

The canonical Int term for a machine integer, in Lean’s representation: ofNat n for n ≥ 0, negSucc (-n-1) below. The Nat argument is a Literal::Nat, not a Succ spine, so a large integer costs one node — which is the whole point of the Nat literal bridge.