`latex/And` := proc( a :: seq( TarskiFormula ), $ )

local ops :: list := [ a ],
      n :: posint := numelems( ops ),
      i :: posint,
      out :: name := `latex/print`( ops[ 1 ] );

for i from 2 to n do # And had at least two operands, this is a real seq

    out := cat( out, ` \\land ` , `latex/print`( ops[ i ] ) );

end do;

sprintf( out );

end proc:

`latex/Or`:= proc( a :: seq( TarskiFormula ) , $ )

local ops :: list := [ a ],
      n :: posint := numelems( ops ),
      i :: posint,
      out :: name := `latex/print`( ops[ 1 ] );

for i from 2 to n do # Or had at least two operands, this is a real seq

    out := cat( out, ` \\lor `, `latex/print`( ops[ i ] ) );

end do;

sprintf( out );

end proc:

`latex/forall` := proc( v :: Or( list( name ), name ), a :: TarskiFormula, $ )

local out :: name := ``,
      x :: name;

if type( v, 'list' ) then

    for x in v do

        out := cat( out, ` \\left( \\forall `, `latex/print`( x ),
                    `\\right)` );

    end do;

else # one variable

    out := cat( out, ` \\left( \\forall `, `latex/print`( v ), `\\right)` );

end if;

if type( op( 0, a ), identical( ':-forall', ':-exists' ) ) then # print the rest

    sprintf( cat( out, `latex/print`( a ) ) );

else # better put in a space

    sprintf( cat( out, `~`, `latex/print`( a ) ) );

end if;

end proc:

`latex/exists` := proc( v :: Or( list( name ), name ), a :: TarskiFormula, $ )

local out :: name := ``,
      x :: name;

if type( v, 'list' ) then

    for x in v do

        out := cat( out, ` \\left( \\exists `, `latex/print`( x ),
                    `\\right)` );

    end do;

else # one variable

    out := cat( out, ` \\left( \\exists `, `latex/print`( v ), `\\right)` );

end if;

if type( op( 0, a ), identical( ':-forall', ':-exists' ) ) then # print the rest

    sprintf( cat( out, `latex/print`( a ) ) );

else # better put in a space

    sprintf( cat( out, `~`, `latex/print`( a ) ) );

end if;

end proc:

`latex/Implies` := proc( a :: TarskiFormula, b :: TarskiFormula, $ )

sprintf( cat ( `latex/print`( a ), ` \\Rightarrow `, `latex/print`( b ) ) );

end proc: