DefinitionsCore, allowAutoName, attrs, doc, dontTranslate, existing, none, ref, relevantArg?, rename, reorder?, self, tgt, RelevantArg, ReplacementM, run, TranslateData, attrName, changeNumeral, doTranslateAttr, guessNameData, ignoreArgsAttr, isDual, translations, unfoldBoundaries?, TranslationInfo, relevantArg, reorder, translation, addTranslationAttr, applyAttributes, applyReplacementForall, applyReplacementFun, applyReplacementLambda, attrArgs, attrOption, bracketedOption, checkExistingType, copyInstanceAttribute, copyMetaData, declUnfoldSimpAuxLemmas, dontTranslateOption, elabRename, elabTranslationAttr, etaExpandN, findAuxDecls, findPrefixTranslation?, findTargetName, findTranslation?, findTranslationName?, getRelevantArg, insertTranslation, instBEqRelevantArg, beq, instInhabitedRelevantArg, default, instToMessageDataRelevantArg, existingAttributeWarning, translateExisting, translateGenerateName, translateOverwrite, translateRedundant, translateRelevantArg, translateReorder, proceedFields, proceedFieldsAux, relevantArgOption, renameBinderNames, renameOption, renameRule, reorderOption, shouldTranslate, targetName, transformDeclRec, translateLemmas, translationHint, updateAndAddDecl, updateDecl, warnAttr, warnAttrCore, warnParametricAttr, Core, Core, Core, Core | 85 |