Function register_inductive_int 

pub fn register_inductive_int(ctx: &mut Context) -> KernelResult<()>

The whole adoption, as one call: Int gains Lean’s two constructors and Lean’s arithmetic.

Nat must already be registered (Int_ofNat stores a Nat); StandardLibrary::register calls this once Nat and its arithmetic exist. It defines Int_add/Int_sub/Int_mul/ Int_le and leaves the public add/sub/mul names alone — binding those to these definitions is register_public_arithmetic_aliases, a separate step with its own check.

use logicaffeine_kernel::int_inductive::canonical_int;
use logicaffeine_kernel::prelude::StandardLibrary;
use logicaffeine_kernel::{normalize, Term};

let ctx = StandardLibrary::context();
let constructors: Vec<&str> = ctx.get_constructors("Int").into_iter().map(|(name, _)| name).collect();
assert_eq!(constructors, ["Int_ofNat", "Int_negSucc"]);

let app = |f: Term, x: Term| Term::App(Box::new(f), Box::new(x));
let sum = app(app(Term::Global("Int_add".into()), canonical_int(2)), canonical_int(-5));
assert_eq!(normalize(ctx, &sum), canonical_int(-3));