Logiweb aspects of peano free * set * to * end free in pyk

Up Help

The predefined "pyk" aspect

define pyk of peano free var a set var x to var b end free as text unicode start of text unicode small p unicode small e unicode small a unicode small n unicode small o unicode space unicode small f unicode small r unicode small e unicode small e unicode space unicode asterisk unicode space unicode small s unicode small e unicode small t unicode space unicode asterisk unicode space unicode small t unicode small o unicode space unicode asterisk unicode space unicode small e unicode small n unicode small d unicode space unicode small f unicode small r unicode small e unicode small e unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of peano free var a set var x to var b end free as text unicode start of text unicode newline unicode backslash unicode small d unicode small o unicode small t unicode left brace unicode small f unicode small r unicode small e unicode small e unicode right brace unicode backslash unicode small l unicode small a unicode small n unicode small g unicode small l unicode small e unicode space unicode number sign unicode one unicode period unicode newline unicode vertical line unicode space unicode number sign unicode two unicode period unicode newline unicode colon unicode equal sign unicode space unicode number sign unicode three unicode period unicode newline unicode backslash unicode small r unicode small a unicode small n unicode small g unicode small l unicode small e unicode end of text end unicode text end text end define

The predefined "value" aspect

define value of peano free var a set var x to var b end free as var x tagged guard ( var b tagged guard newline tagged if var a is peano var then true else newline tagged if not ( var a term root equal quote peano all var u indeed var v end quote ) then peano free star var a tail set var x to var b end free else newline tagged if var a first term equal var x then true else newline tagged if peano nonfree var x in var a second end nonfree then true else newline tagged if not peano nonfree var a first in var b end nonfree then false else newline peano free var a second set var x to var b end free end if end if end if end if end if ) end define