Logiweb aspects of peano nonfree * in * end nonfree in pyk

Up Help

The predefined "pyk" aspect

define pyk of peano nonfree var x in var y end nonfree 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 n unicode small o unicode small n unicode small f unicode small r unicode small e unicode small e unicode space unicode asterisk unicode space unicode small i unicode small n unicode space unicode asterisk unicode space unicode small e unicode small n unicode small d unicode space unicode small n unicode small o unicode small n 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 nonfree var x in var y end nonfree as text unicode start of text unicode newline unicode backslash unicode small d unicode small o unicode small t unicode left brace unicode small n unicode small o unicode small n unicode small f unicode small r unicode small e unicode small e unicode right brace unicode left parenthesis unicode number sign unicode one unicode period unicode newline unicode comma unicode number sign unicode two unicode period unicode newline unicode right parenthesis unicode end of text end unicode text end text end define

The predefined "value" aspect

define value of peano nonfree var x in var y end nonfree as newline tagged if var y is peano var then not ( var x term equal var y ) else newline tagged if not ( var y term root equal quote peano all var x indeed var y end quote ) then peano nonfree star var x in var y tail end nonfree else newline tagged if var x term equal ( var y first ) then true else peano nonfree var x in var y second end nonfree end if end if end if end define