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]