pub const DEFAULT_INSTANCE_PRIORITY: i64 = 1000;Expand description
Lean’s default instance priority — what instance foo : C α := … gets when it says no
(priority := n). Named rather than spelled 1000 at each site so a translator carrying a
Lean source’s explicit priorities lands them on the same scale.