Lean4
/-- Dictionary used by `guessName` to autogenerate names.
Note: `guessName` capitalizes first element of the output according to
capitalization of the input. Input and first element should therefore be lower-case,
2nd element should be capitalized properly.
-/
def nameDict : String → List String
| "one" => ["zero"]
| "mul" => ["add"]
| "smul" => ["vadd"]
| "inv" => ["neg"]
| "div" => ["sub"]
| "prod" => ["sum"]
| "hmul" => ["hadd"]
| "hsmul" => ["hvadd"]
| "hdiv" => ["hsub"]
| "hpow" => ["hsmul"]
| "finprod" => ["finsum"]
| "tprod" => ["tsum"]
| "pow" => ["nsmul"]
| "npow" => ["nsmul"]
| "zpow" => ["zsmul"]
| "mabs" => ["abs"]
| "monoid" => ["add", "Monoid"]
| "submonoid" => ["add", "Submonoid"]
| "group" => ["add", "Group"]
| "subgroup" => ["add", "Subgroup"]
| "semigroup" => ["add", "Semigroup"]
| "magma" => ["add", "Magma"]
| "haar" => ["add", "Haar"]
| "prehaar" => ["add", "Prehaar"]
| "unit" => ["add", "Unit"]
| "units" => ["add", "Units"]
| "cyclic" => ["add", "Cyclic"]
| "rootable" => ["divisible"]
| "semigrp" => ["add", "Semigrp"]
| "grp" => ["add", "Grp"]
| "commute" => ["add", "Commute"]
| "semiconj" => ["add", "Semiconj"]
| "zpowers" => ["zmultiples"]
| "powers" => ["multiples"]
| "multipliable" => ["summable"]
| "gpfree" => ["apfree"]
| "quantale" => ["add", "Quantale"]
| "square" => ["even"]
| "mconv" => ["conv"]
| "irreducible" => ["add", "Irreducible"]
| "mlconvolution" => ["lconvolution"]
| x => [x]
