doc-src/Intro/advanced.tex
changeset 348 1f5a94209c97
parent 331 13660d5f6a77
child 459 03b445551763
equal deleted inserted replaced
347:cd41a57221d0 348:1f5a94209c97
   544 \begin{ttbox}
   544 \begin{ttbox}
   545 consts and,or :: "gate"
   545 consts and,or :: "gate"
   546        negate :: "signal => signal"
   546        negate :: "signal => signal"
   547 \end{ttbox}
   547 \end{ttbox}
   548 
   548 
   549 \subsection{Infix and Mixfix operators}
   549 \subsection{Infix and mixfix operators}
   550 \index{infixes}\index{examples!of theories}
   550 \index{infixes}\index{examples!of theories}
   551 
   551 
   552 Infix or mixfix syntax may be attached to constants.  Consider the
   552 Infix or mixfix syntax may be attached to constants.  Consider the
   553 following theory:
   553 following theory:
   554 \begin{ttbox}
   554 \begin{ttbox}
   673 declaring certain types to be of class $arith$.  For example, let us
   673 declaring certain types to be of class $arith$.  For example, let us
   674 declare the 0-place type constructors $bool$ and $nat$:
   674 declare the 0-place type constructors $bool$ and $nat$:
   675 \index{examples!of theories}
   675 \index{examples!of theories}
   676 \begin{ttbox}
   676 \begin{ttbox}
   677 BoolNat = Arith +
   677 BoolNat = Arith +
   678 types   bool,nat
   678 types   bool  nat
   679 arities bool,nat    :: arith
   679 arities bool, nat   :: arith
   680 consts  Suc         :: "nat=>nat"
   680 consts  Suc         :: "nat=>nat"
   681 \ttbreak
   681 \ttbreak
   682 rules   add0        "0 + n = n::nat"
   682 rules   add0        "0 + n = n::nat"
   683         addS        "Suc(m)+n = Suc(m+n)"
   683         addS        "Suc(m)+n = Suc(m+n)"
   684         nat1        "1 = Suc(0)"
   684         nat1        "1 = Suc(0)"