Literal

class proveit.Literal(string_format, latex_format=None, *, extra_core_info=(), theory=None, fence_when_forced=False, styles=None)[source]

Bases: proveit.Label

A Literal expresses contextual meaning. Such Labels are not interchangeable. The Literal must be associated with a ‘theory’ that should be the name of a package. Through Axiom elimination, a Literal may be converted to the Variable with the same label.

Attributes Summary

instances

Methods Summary

as_variable(self)

Return the var with the same label as this Literal.

instance(theory, string_format, latex_format)

remake_arguments(self)

Yield the argument values that could be used to recreate the Label.

Attributes Documentation

instances = {-9188385170902601674: subset_eq, -9003481430565431444: d, -8439815357827109191: Functions, -8126841752215078577: TRUE, -8038872073367672751: log, -7587779112643035189: forall, -7570205036782169115: RealPos, -7569689981655815965: Bijections, -7551651125200454813: Natural, -7304896785106943938: Sum, -7271146994296278777: X, -7173601073969823930: length, -7161001076611970004: CartExp, -6974530005661929865: Prod, -6812821953514892167: 7, -6624127300895153634: union_of_all, -6313285087494102444: INV_IMAGE, -6243323438261144260: emptyset, -6226060393467027420: +, -6095871450253213856: e, -6067426738545350194: IntervalOC, -5948225686732291227: card, -5691337509700032988: union, -5557494259094284149: 9, -5477260966565707128: mod, -5476882772187139509: disjoint, -5280406617637333655: IntervalOO, -5258793760129526778: Digits, -5129884787866768469: RationalNonNeg, -4798670074930044274: a, -4671271784690680497: not_subset_eq, -4635931211406523317: Rings, -4407668292204400274: 1, -4405014782946025746: *, -4339031376692069716: Max, -4263209124192027121: IntegerNonZero, -4178273158830259266: intersect, -3982185123726221558: =>, -3795710419666672013: in, -3737290963947554471: ModAbs, -3610036356356854389: RationalPos, -3578863820886012702: power_set, -3533574092746696039: RealNonPos, -2894950609755654544: Bits, -2780452028251140455: 8, -2707935974164508365: RationalNonPos, -2474977051154139925: infinity, -2388524273886544420: RationalNeg, -2245090951212296811: RealNonNeg, -2123635678226522333: Interval, -2102364033274972415: RationalNonZero, -1251627907292522104: equiv, -893252273679098704: in_c, -750567837080616797: =, -465799328805318953: Integer, -351338937222182384: 5, -232530442840450244: IntegerNeg, -228276507541578023: Exp, -210367017954877534: MonDecFuncs, -188083685237640908: IntervalCO, -125085544009771776: Fields, 253316268511229502: pi, 272440630622740376: 2, 299081763086127485: o, 349701043018531660: and, 393051751343153733: <=>, 475250402188251258: Groups, 573560726221140351: gcd, 841302987857381137: floor, 865334261652415542: Integrate, 872357167105775047: not-in_{C}, 1080500750294472932: <=, 1293988675404789519: i, 1396415828159297042: Min, 1446539470235168817: CondSet, 1532640125768961250: Complex, 1554912308510187755: not_equiv, 1636546983177269445: <, 1713218671844482245: ComplexNonZero, 1953059431054502348: or, 2152729143567661262: SetOfAll, 2321323219432000463: Set, 2638941415373696352: not, 2988921540524970592: not_proper_subset, 3005418092880861093: IntegerNonPos, 3512141477093358250: round, 4187432800468057631: NaturalPos, 4268239463504999805: notexists, 4396497216684803671: Rational, 4413790853794904241: -, 4456919683355210789: 4, 4801904830104223426: ceil, 5152705945605650150: -, 5205331168563772069: Surjections, 5231074764238696147: Injections, 5401587859233054638: proper_subset, 5502370859557011068: e, 5678178871847591955: Real, 5998254043090330457: b, 6147948091530686974: 6, 6431728340730280254: 0, 6732600581293238703: exists, 6848425575416631454: RealNonZero, 7290818550574328888: |, 7379648194459824553: Decimal, 7494050649207257115: BOOLEAN, 7510158498894747315: f, 7512961495426454284: |, 7537208906286420322: Binary, 7551729174851985121: intersect_all, 7618601218131959339: IMAGE, 7630393467088643789: /, 7848318698973315836: Abs, 8027589656618542560: RealNeg, 8100241845314268225: !=, 8226949363912417483: IntervalCC, 8285451244390463497: distinct, 8340103599963261188: c, 8546274404819141232: FALSE, 8984601993211801543: 3, 9026939636064535346: not-in}

Methods Documentation

as_variable(self)[source]

Return the var with the same label as this Literal.

classmethod instance(theory, string_format, latex_format)[source]
remake_arguments(self)

Yield the argument values that could be used to recreate the Label. This is a default for simple Labels, Variables, or Literals.