pyk.prelude.ml module

is_bottom(term: KInner, *, weak: bool = False) → bool[source]

is_top(term: KInner, *, weak: bool = False) → bool[source]

mlAnd(conjuncts: Iterable[KInner], sort: str | KSort = KSort(name='GeneratedTopCell')) → KInner[source]

mlBottom(sort: str | KSort = KSort(name='GeneratedTopCell')) → KApply[source]

mlCeil(term: KInner, arg_sort: str | KSort = KSort(name='GeneratedTopCell'), sort: str | KSort = KSort(name='GeneratedTopCell')) → KApply[source]

mlEquals(term1: KInner, term2: KInner, arg_sort: str | KSort = KSort(name='K'), sort: str | KSort = KSort(name='GeneratedTopCell')) → KApply[source]

mlEqualsFalse(term: KInner, sort: str | KSort = KSort(name='GeneratedTopCell')) → KApply[source]

mlEqualsTrue(term: KInner, sort: str | KSort = KSort(name='GeneratedTopCell')) → KApply[source]

mlExists(var: KVariable, body: KInner, sort1: str | KSort = KSort(name='KItem'), sort2: str | KSort = KSort(name='GeneratedTopCell')) → KApply[source]

mlImplies(antecedent: KInner, consequent: KInner, sort: str | KSort = KSort(name='GeneratedTopCell')) → KApply[source]

mlNot(term: KInner, sort: str | KSort = KSort(name='GeneratedTopCell')) → KApply[source]

mlOr(disjuncts: Iterable[KInner], sort: str | KSort = KSort(name='GeneratedTopCell')) → KInner[source]

mlTop(sort: str | KSort = KSort(name='GeneratedTopCell')) → KApply[source]