Literal

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

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 = {-8617750114071635156: not, -8501160225742536928: c, -8299186304191231923: MonDecFuncs, -8215147899766557163: union_of_all, -7937572143781572070: <=>, -7529716159000027974: Integer, -7344850798544984164: not_proper_subset, -7176117891114577461: intersect_all, -6683207489017337211: 2, -6658757120311696419: Real, -6596907545778216611: not-in, -6518467482470655242: or, -6424756816658790195: Surjections, -6423399564188127109: 3, -6419225540000411849: 7, -6103878685217680764: |, -5885489860933318806: not_subset_eq, -5818349017240752844: b, -5773228978178022564: Digits, -5591110866595108179: o, -5278666621008562001: RealNonPos, -5066813675848406669: IntervalOO, -4958737773995044906: infinity, -4720513412215392686: Prod, -4316447756305579052: =, -4272102976990172730: Binary, -3873121932304203981: Functions, -3758767900713865025: subset_eq, -3683576451349442126: Set, -3173342123285482618: floor, -3054290589209901242: ModAbs, -3024496117635877371: Bijections, -2914764172912850372: Abs, -2859811161136320712: 6, -2818551124372427645: Bits, -2628629277522432359: disjoint, -2546773599955493306: RealNonNeg, -2468483153205908710: BOOLEAN, -1976107513673060153: notexists, -1917147509614043375: IntervalCO, -1829334552917510075: Kdelta, -1370008103119456053: RationalPos, -1205111099992528359: Max, -1048441784526174290: and, -945346850270280144: 4, -938360155153791705: IntegerNonZero, -773687128592410437: 8, -330775533633179923: *, -214084819720594490: NaturalPos, -194361343232398652: Natural, -70451389580157051: 9, -70284424704035375: conj, 269659708905909779: -, 386823568785661561: RationalNonPos, 840739094875647414: i, 1326563759391808308: equiv, 1429412625897165420: f, 1566438235666990394: distinct, 1721481226873117400: 1, 1780044630185095017: |, 1780094200298596197: Sum, 1791654282864648389: intersect, 1814169741764535961: Exp, 1948934716605769574: RealNeg, 1954458090677477769: Min, 1966578238362248426: in_c, 2054844730221136023: <, 2238634103526679832: RationalNonNeg, 2379876497939125247: Fields, 2402922382964519523: emptyset, 2533318301803512462: ceil, 2621352481562408027: in, 2752690086573881110: Groups, 2784483964871030420: RationalNeg, 2841900610713693061: log, 3002209755895095006: not_equiv, 3056394053428936479: a, 3070079684954699739: -, 3261123290971701058: card, 3273672570378159492: not-in_{C}, 3344639364020337828: CartExp, 3469844606715823709: IntegerNonPos, 3550622752969491547: Interval, 3601122293905889130: Decimal, 3853645754430690213: RealNonZero, 3898422872416151191: length, 3929908493919527253: Injections, 4377885864059127159: power_set, 4442962864091817453: INV_IMAGE, 4490330106216093748: CondSet, 4499082549434943909: union, 4525779906463669288: proper_subset, 4533105014200550256: d, 4631884731986072628: IntervalCC, 4754828282409008602: Complex, 4923192943207757036: mod, 4933172930579023816: ComplexNonZero, 4941750635618572998: SetOfAll, 4971959485861118670: TRUE, 5022147937150007349: IMAGE, 5373757163458481863: =>, 5384316408665657235: !=, 5450140835226777681: Integrate, 5618430022634514232: IntervalOC, 5661297186805217080: X, 5921266480678332337: 0, 6347925644083319746: exists!, 6395809814281474150: FALSE, 6402487056546526194: RationalNonZero, 6729262995259653117: 5, 6767434025217811287: RealPos, 6778430407371689834: pi, 7001025259303047762: Rational, 7044732841237167025: <=, 7669555949913650869: round, 7678020119075569841: Rings, 7732539476907971637: IntegerNeg, 8093509342840966994: +, 8130164520588137599: e, 8239637463043666329: e, 8356149115555945842: gcd, 8523727244626458389: exists, 8907672190725801409: forall, 9183301453250817066: /}

Methods Documentation

as_variable(self)

Return the var with the same label as this Literal.

classmethod instance(theory, string_format, latex_format)

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.