pub fn register_int_constructors(ctx: &mut Context) -> KernelResult<()>Expand description
Int’s two constructors, through the CHECKED door.
ofNat : Nat → Int and negSucc : Nat → Int, in Lean’s declaration order
(Init/Data/Int/Basic.lean:42, :45) — order is the whole content of a declaration here,
because Term::Match is positional.