# LatticeJoinOfMeets¶

logic.spad line 3571 [edit on github]

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

- _|_: %

- atom?: % -> Boolean
returns

`true`

if this is an atom, that is a leaf node otherwise return`false`

if this is a compound term

- coerce: % -> LatticeMeetOfJoins
convert lattice from join-of-meets to meet-of-joins

- coerce: % -> OutputForm
from CoercibleTo OutputForm

- coerce: LatticeMeetOfJoins -> %
convert lattice from meet-of-joins to join-of-meets

- 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 []

- join: List % -> %
`join of`

set of elements

- latex: % -> String
from SetCategory

- latticeJoinOfMeets: 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: %

- 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