pyk.prelude.ml module¶

is_bottom(term: KInner) → bool[source]¶

is_top(term: KInner) → 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='GeneratedTopCell'), 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, sort: 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]¶