| imaxUniv | Language.Lean.Univ, Language.Lean |
| IndexName | Language.Lean.Internal.Name, Language.Lean.Name, Language.Lean |
| InductiveDecl | Language.Lean.Internal.Inductive, Language.Lean.Inductive |
| inductiveDecl | Language.Lean.Inductive |
| inductiveDeclNumParams | Language.Lean.Inductive |
| InductiveDeclPtr | Language.Lean.Internal.Inductive |
| inductiveDeclTypes | Language.Lean.Inductive |
| inductiveDeclUnivParams | Language.Lean.Inductive |
| InductiveType | Language.Lean.Internal.Inductive, Language.Lean.Inductive |
| inductiveType | Language.Lean.Inductive |
| inductiveTypeConstructors | Language.Lean.Inductive |
| inductiveTypeHasDepElim | Language.Lean.Inductive |
| inductiveTypeName | Language.Lean.Inductive |
| InductiveTypePtr | Language.Lean.Internal.Inductive |
| inductiveTypeType | Language.Lean.Inductive |
| inferType | Language.Lean.Typechecker, Language.Lean |
| instantiateUniv | Language.Lean.Univ, Language.Lean |
| instantiateUniv2 | Language.Lean.Univ, Language.Lean |
| intOption | Language.Lean.Options, Language.Lean |
| IOState | Language.Lean.Internal.IOS, Language.Lean.IOS, Language.Lean |
| IOStateType | Language.Lean.Internal.IOS, Language.Lean.IOS, Language.Lean |
| IOStateTypeRepr | Language.Lean.IOS, Language.Lean |
| isDefEq | Language.Lean.Typechecker, Language.Lean |
| IsLeanValue | Language.Lean.Internal.Exception |
| IsList | Language.Lean.List, Language.Lean |
| IsListIso | Language.Lean.List, Language.Lean |
| Item | Language.Lean.List, Language.Lean |