Logiweb aspects of conclude four * lemma * end conclude in pyk

Up Help

The predefined "pyk" aspect

define pyk of conclude four var a lemma var l end conclude as text unicode start of text unicode small c unicode small o unicode small n unicode small c unicode small l unicode small u unicode small d unicode small e unicode space unicode small f unicode small o unicode small u unicode small r unicode space unicode asterisk unicode space unicode small l unicode small e unicode small m unicode small m unicode small a unicode space unicode asterisk unicode space unicode small e unicode small n unicode small d unicode space unicode small c unicode small o unicode small n unicode small c unicode small l unicode small u unicode small d unicode small e unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of conclude four var a lemma var l end conclude as text unicode start of text unicode newline unicode small c unicode small o unicode small n unicode small c unicode small l unicode small u unicode small d unicode small e unicode underscore unicode four unicode space unicode left parenthesis unicode space unicode number sign unicode one unicode period unicode newline unicode comma unicode space 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 conclude four var a lemma var l end conclude as var a tagged guard ( var l tagged guard newline tagged if not ( var l term root equal quote all var x indeed var y end quote ) then var a else newline let one lambda var v dot all var v indeed conclude four var a at var v lemma var l second end conclude apply quote metavar x end metavar end quote root pair ( var l first pair true ) end let end if ) end define