# LatticeJoinOfMeetsΒΆ

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: % -> LatticeMeetOfJoins
- convert lattice from join-of-meets to meet-of-joins

- coerce: % -> OutputForm
- output

- 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 []
- hash: % -> SingleInteger
- from SetCategory
- hashUpdate!: (HashState, %) -> HashState
- from SetCategory

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