Logiweb(TM)

6.7.4 Layout

Prev Up Next Page 90 of 800 Search internet


Recall multzero.lgs:

     1	"";;014E20344F3D486370710A10269E83D974EB8E9787EFB994A0BBD8BB0806
     2	""P multzero
     3	""R check
     4	""R Peano
     5	""R base
     6	
     7	""D 0
     8	3.2l
     9	
    10	""B
    11	page ( ""N , ""C )
    12	title "Multiplication by zero"
    13	bib "
    14	@Book         {Mendelson87,
    15	  author    = {E. Mendelson},
    16	  title     = {Introduction to Mathematical Logic},
    17	  publisher = {Wadsworth and Brooks},
    18	  year      = {1987},
    19	  edition   = {3.}}
    20	"
    21	main text "
    22	\title{Multiplication by zero}
    23	\author{A. U. Thor}
    24	\maketitle
    25	\tableofcontents
    26	"[ make macro expanded version ragged right ]"
    27	"[ prepare proof indentation ]"
    28	\section{Theorem}
    29	We now state Lemma 3.2l of \cite{Mendelson87}:
    30	"[ PA lemma 3.2l : all x : 0 * x = 0 end lemma ]"
    31	\section{Proof}
    32	"[ PA proof of 3.2l :
    33	line L01 : S7 >> 0 * 0 = 0 ;
    34	line L02 : Block >> Begin ;
    35	line L03 : Hypothesis >> 0 * x = 0 ;
    36	line L04 : S8 >> 0 * x suc = 0 * x + 0 ;
    37	line L05 : S5 >> 0 * x + 0 = 0 * x ;
    38	line L06 : 3.2c mp L04 mp L05 >> 0 * x suc = 0 * x ;
    39	line L07 : 3.2c mp L06 mp L03 >> 0 * x suc = 0 ;
    40	line L08 : Block >> End ;
    41	line L09 : Induction at x ponens L01 ponens L08 >> 0 * x = 0 ;
    42	line L10 : Gen1 ponens L09 >> all x : 0 * x = 0 qed ]"
    43	\bibliography{./page}
    44	"
    45	appendix "
    46	\title{Multiplication by zero - appendix}
    47	\author{A. U. Thor}
    48	\maketitle
    49	\tableofcontents
    50	\section{\TeX\ definitions}
    51	\begin{statements}
    52	\item "[[ tex show define 3.2l as "
    53	\mathbf{3.2l}" end define ]]"
    54	\end{statements}
    55	"
    56	end page
    57	

Line 27 ensures that proof are indented correctly. You must include 'prepare proof indentation' on all pages that contain proofs. Otherwise you will get an error running latex and the relevant .log file will tell you that \indentation is undefined. You can see indentation at work in Line L03-L07:

prepare proof indentation,PA proof of 3.2l : line L01 : S7 >> 0 * 0 = 0 ; line L02 : Block >> Begin ; line L03 : Hypothesis >> 0 * x = 0 ; line L04 : S8 >> 0 * x suc = 0 * x + 0 ; line L05 : S5 >> 0 * x + 0 = 0 * x ; line L06 : 3.2c mp L04 mp L05 >> 0 * x suc = 0 * x ; line L07 : 3.2c mp L06 mp L03 >> 0 * x suc = 0 ; line L08 : Block >> End ; line L09 : Induction at x ponens L01 ponens L08 >> 0 * x = 0 ; line L10 : Gen1 ponens L09 >> all x : 0 * x = 0 qed

Line 26 ensures that if one renders the macro expanded version of the body, then the result will look tolerable. The version 0.0.x and 0.1.x series of Logiweb always rendered the expansion as a debugging aid. The feature turned out not to be very useful. From the 0.2.x series it is up to the user whether or not the macro expanded version should be rendered, and chances are users will choose not to render it. Thus, you do not need to include something like Line 26 in your own pages, but it is retained in the multzero page for the sake of backports.

Prev Up Next Page 90 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05