LatticeMeetOfJoinsΒΆ

logic.spad line 3356

parse result includes term returned and new index

/\: (%, %) -> %
from MeetSemilattice
=: (%, %) -> Boolean
returns true (boolean true) if intuitionisticLogic values are the same. Translates from Intuitionistic Logic to Boolean Logic
\/: (%, %) -> %
from JoinSemilattice
_|_: %
from BoundedJoinSemilattice
~=: (%, %) -> Boolean
from BasicType
atom?: % -> Boolean
returns true if this is an atom, that is a leaf node otherwise return false if this is a compound term
coerce: % -> OutputForm
output
deductions: List % -> List %
assumes ln contains a list of factors which must be true for the whole to be true (such as the list produced by factor). From this deductions attempts to produce a list of other proposition that must also be true by using modus ponens. This is used to determine the returned type when converting ILogic to types by using the Curry-Howard isomorphism.
empty?: % -> Boolean
true if empty
emptyLattice: () -> %
construct an empty lattice
factor: % -> List %
splits n into a list of factors which must be true for the whole to be true. This assumes that the top level is already a set of factors separated by /\ otherwise the result will just be a list with one entry: 'n'. This is used when converting ILogic to types by using the Curry-Howard isomorphism.
getChildren: % -> List %
returns child nodes if this is a compound term otherwise returns []
hash: % -> SingleInteger
from SetCategory
hashUpdate!: (HashState, %) -> HashState
from SetCategory
join: List % -> %
join of set of elements
latex: % -> String
from SetCategory
latticeMeetOfJoins: Union(const: Record val: Symbol, var: Record str: String) -> %
construct a lattice with one element
logicF: () -> %
construct false (contradiction): a logical constant.
logicT: () -> %
construct true: a logical constant.
meet: List % -> %
meet of set of elements
opType: % -> Symbol
if this is a compound op then opType returns the type of that op: “IMPLY”::Symbol =implies “AND”::Symbol=/”OR”::Symbol=\/ “NOT”::Symbol=~ “OTHER”::Symbol=not compound op
redux: % -> %
attempt to simplify terms
T: %
from BoundedMeetSemilattice
toString: % -> String
creates a string representation of this term and its sub-terms
toStringUnwrapped: % -> String
similar to ‘toString’ but does not put outer compound terms in brackets
value: % -> Symbol
returns: “T”::Symbol = T “F”::Symbol = _|_ “E”::Symbol = error “P”::Symbol = proposition “C”::Symbol = compound Constructs lambda term and bind any variables with the name provided
variable: String -> %
construct a variable

BasicType

BoundedDistributiveLattice

BoundedJoinSemilattice

BoundedLattice

BoundedMeetSemilattice

CoercibleTo OutputForm

DistributiveLattice

JoinSemilattice

Lattice

MeetSemilattice

SetCategory