Equations
- Lean.addProtected env n = Lean.protectedExt.tag env n
Instances For
Equations
- Lean.isProtected env n = Lean.protectedExt.isTagged env n
Instances For
Equations
Instances For
Equations
- Lean.isPrivateNameFromImportedModule env n = match Lean.privateToUserName? n with | some userName => Lean.mkPrivateName env userName != n | x => false