UnicodeLinter
📁 Source: Mathlib/Tactic/Linter/TextBased/UnicodeLinter.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsprintCodepointHex, printCodepointHex, emoji, text, emojis, isAllowedCharacter, nonEmojis, replaceDisallowed | 8 |
| Theorems | 0 |
| Total | 8 |
Mathlib.Linter.TextBased.UnicodeLinter
Definitions
| Name | Category | Theorems |
|---|---|---|
emojis 📖 | CompOp | — |
isAllowedCharacter 📖 | CompOp | — |
nonEmojis 📖 | CompOp | — |
replaceDisallowed 📖 | CompOp | — |
Mathlib.Linter.TextBased.UnicodeLinter.Char
Definitions
| Name | Category | Theorems |
|---|---|---|
printCodepointHex 📖 | CompOp | — |
Mathlib.Linter.TextBased.UnicodeLinter.String
Definitions
| Name | Category | Theorems |
|---|---|---|
printCodepointHex 📖 | CompOp | — |
Mathlib.Linter.TextBased.UnicodeLinter.UnicodeVariant
Definitions
| Name | Category | Theorems |
|---|---|---|
emoji 📖 | CompOp | — |
text 📖 | CompOp | — |
---