##
Logiweb aspects of proof define " as " end define in pyk

Up
Help

###
The "pyk" aspect

Define pyk of proof define asterisk as asterisk end define as "proof define "! as "! end define" end define

###
The "tex" aspect

Define tex of proof define x as y end define as "

[ "[ texname x end texname ] { "

\stackrel{proof}{=} "[ texname y end texname ]"

]" } end define

###
The "macro" aspect

define macro of proof define x as y end define as \ x . expand ( quote macro define proof define x as y end define as define proof of x as y end define end define end quote , x ) end define

###
The "locate/kg" aspect

define locate of proof define x as y end define as "proof" :: 1 end define

The pyk compiler,
version 0.1.9 by
Klaus Grue,

GRD-2007-07-12.UTC:20:11:58.175987
=
MJD-54293.TAI:20:12:31.175987
=
LGT-4690987951175987e-6