Lean4
/-- There are a few abbreviations we use. For example "Nonneg" instead of "ZeroLE"
or "addComm" instead of "commAdd".
Note: The input to this function is case sensitive!
Todo: A lot of abbreviations here are manual fixes and there might be room to
improve the naming logic to reduce the size of `fixAbbreviation`.
-/
def fixAbbreviation : List String → List String
| "is" :: "Cancel" :: "Add" :: s => "isCancelAdd" :: fixAbbreviation s
| "Is" :: "Cancel" :: "Add" :: s => "IsCancelAdd" :: fixAbbreviation s
| "is" :: "Left" :: "Cancel" :: "Add" :: s => "isLeftCancelAdd" :: fixAbbreviation s
| "Is" :: "Left" :: "Cancel" :: "Add" :: s => "IsLeftCancelAdd" :: fixAbbreviation s
| "is" :: "Right" :: "Cancel" :: "Add" :: s => "isRightCancelAdd" :: fixAbbreviation s
| "Is" :: "Right" :: "Cancel" :: "Add" :: s => "IsRightCancelAdd" :: fixAbbreviation s
| "cancel" :: "Add" :: s => "addCancel" :: fixAbbreviation s
| "Cancel" :: "Add" :: s => "AddCancel" :: fixAbbreviation s
| "left" :: "Cancel" :: "Add" :: s => "addLeftCancel" :: fixAbbreviation s
| "Left" :: "Cancel" :: "Add" :: s => "AddLeftCancel" :: fixAbbreviation s
| "right" :: "Cancel" :: "Add" :: s => "addRightCancel" :: fixAbbreviation s
| "Right" :: "Cancel" :: "Add" :: s => "AddRightCancel" :: fixAbbreviation s
| "cancel" :: "Comm" :: "Add" :: s => "addCancelComm" :: fixAbbreviation s
| "Cancel" :: "Comm" :: "Add" :: s => "AddCancelComm" :: fixAbbreviation s
| "comm" :: "Add" :: s => "addComm" :: fixAbbreviation s
| "Comm" :: "Add" :: s => "AddComm" :: fixAbbreviation s
| "Zero" :: "LE" :: s => "Nonneg" :: fixAbbreviation s
| "zero" :: "_" :: "le" :: s => "nonneg" :: fixAbbreviation s
| "zero" :: "LE" :: s => "nonneg" :: fixAbbreviation s
| "Zero" :: "LT" :: s => "Pos" :: fixAbbreviation s
| "zero" :: "_" :: "lt" :: s => "pos" :: fixAbbreviation s
| "zero" :: "LT" :: s => "pos" :: fixAbbreviation s
| "LE" :: "Zero" :: s => "Nonpos" :: fixAbbreviation s
| "le" :: "_" :: "zero" :: s => "nonpos" :: fixAbbreviation s
| "LT" :: "Zero" :: s => "Neg" :: fixAbbreviation s
| "lt" :: "_" :: "zero" :: s => "neg" :: fixAbbreviation s
| "Add" :: "Single" :: s => "Single" :: fixAbbreviation s
| "add" :: "Single" :: s => "single" :: fixAbbreviation s
| "add" :: "_" :: "single" :: s => "single" :: fixAbbreviation s
| "Add" :: "Support" :: s => "Support" :: fixAbbreviation s
| "add" :: "Support" :: s => "support" :: fixAbbreviation s
| "add" :: "_" :: "support" :: s => "support" :: fixAbbreviation s
| "Add" :: "TSupport" :: s => "TSupport" :: fixAbbreviation s
| "add" :: "TSupport" :: s => "tsupport" :: fixAbbreviation s
| "add" :: "_" :: "tsupport" :: s => "tsupport" :: fixAbbreviation s
| "Add" :: "Indicator" :: s => "Indicator" :: fixAbbreviation s
| "add" :: "Indicator" :: s => "indicator" :: fixAbbreviation s
| "add" :: "_" :: "indicator" :: s => "indicator" :: fixAbbreviation s
| "is" :: "Even" :: s => "even" :: fixAbbreviation s
| "Is" :: "Even" :: s => "Even" :: fixAbbreviation s
| "is" :: "Regular" :: s => "isAddRegular" :: fixAbbreviation s
| "Is" :: "Regular" :: s => "IsAddRegular" :: fixAbbreviation s
| "is" :: "Left" :: "Regular" :: s => "isAddLeftRegular" :: fixAbbreviation s
| "Is" :: "Left" :: "Regular" :: s => "IsAddLeftRegular" :: fixAbbreviation s
| "is" :: "Right" :: "Regular" :: s => "isAddRightRegular" :: fixAbbreviation s
| "Is" :: "Right" :: "Regular" :: s => "IsAddRightRegular" :: fixAbbreviation s
| "Has" :: "Fundamental" :: "Domain" :: s => "HasAddFundamentalDomain" :: fixAbbreviation s
| "has" :: "Fundamental" :: "Domain" :: s => "hasAddFundamentalDomain" :: fixAbbreviation s
| "Quotient" :: "Measure" :: s => "AddQuotientMeasure" :: fixAbbreviation s
| "quotient" :: "Measure" :: s => "addQuotientMeasure" :: fixAbbreviation s
| "HSmul" :: s => "HSMul" :: fixAbbreviation s
| "NSmul" :: s => "NSMul" :: fixAbbreviation s
| "Nsmul" :: s => "NSMul" :: fixAbbreviation s
| "ZSmul" :: s => "ZSMul" :: fixAbbreviation s
| "neg" :: "Fun" :: s => "invFun" :: fixAbbreviation s
| "Neg" :: "Fun" :: s => "InvFun" :: fixAbbreviation s
| "unique" :: "Prods" :: s => "uniqueSums" :: fixAbbreviation s
| "Unique" :: "Prods" :: s => "UniqueSums" :: fixAbbreviation s
| "order" :: "Of" :: s => "addOrderOf" :: fixAbbreviation s
| "Order" :: "Of" :: s => "AddOrderOf" :: fixAbbreviation s
| "is" :: "Of" :: "Fin" :: "Order" :: s => "isOfFinAddOrder" :: fixAbbreviation s
| "Is" :: "Of" :: "Fin" :: "Order" :: s => "IsOfFinAddOrder" :: fixAbbreviation s
| "is" :: "Central" :: "Scalar" :: s => "isCentralVAdd" :: fixAbbreviation s
| "Is" :: "Central" :: "Scalar" :: s => "IsCentralVAdd" :: fixAbbreviation s
| "is" :: "Scalar" :: "Tower" :: s => "vaddAssocClass" :: fixAbbreviation s
| "Is" :: "Scalar" :: "Tower" :: s => "VAddAssocClass" :: fixAbbreviation s
| "function" :: "_" :: "add" :: "Semiconj" :: s => "function" :: "_" :: "semiconj" :: fixAbbreviation s
| "function" :: "_" :: "add" :: "Commute" :: s => "function" :: "_" :: "commute" :: fixAbbreviation s
| "Zero" :: "Le" :: "Part" :: s => "PosPart" :: fixAbbreviation s
| "Le" :: "Zero" :: "Part" :: s => "NegPart" :: fixAbbreviation s
| "zero" :: "Le" :: "Part" :: s => "posPart" :: fixAbbreviation s
| "le" :: "Zero" :: "Part" :: s => "negPart" :: fixAbbreviation s
| "Division" :: "Add" :: "Monoid" :: s => "SubtractionMonoid" :: fixAbbreviation s
| "division" :: "Add" :: "Monoid" :: s => "subtractionMonoid" :: fixAbbreviation s
| "Sub" :: "Neg" :: "Zero" :: "Add" :: "Monoid" :: s => "SubNegZeroMonoid" :: fixAbbreviation s
| "sub" :: "Neg" :: "Zero" :: "Add" :: "Monoid" :: s => "subNegZeroMonoid" :: fixAbbreviation s
| "modular" :: "Character" :: s => "addModularCharacter" :: fixAbbreviation s
| "Modular" :: "Character" :: s => "AddModularCharacter" :: fixAbbreviation s
| x :: s => x :: fixAbbreviation s
| [] => []
