compiler/io.github.aplcornell.viaduct.algebra/HeytingAlgebra

HeytingAlgebra

interface HeytingAlgebra<T : HeytingAlgebra<T>> : Lattice<T>

A Heyting algebra is a bounded lattice that supports an implication operation → where A → B is the greatest element x that satisfies A ∧ x ≤ B.

This is also called an implicated lattice.

Functions

imply

abstract infix fun imply(that: T): T

this.imply(that) is the greatest solution to this.meet(x) ≤ that.

join

abstract infix fun join(that: T): T

The least upper bound of this and that.

meet

abstract infix fun meet(that: T): T

The greatest lower bound of this and that.

Inheritors

FreeDistributiveLattice

HeytingAlgebra

See also

Functions

Inheritors