[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Latex generation problem with TABLE construct


I have defined a function using the TABLE construct:

% Describe OR gate
  orf(v,w:DIGIT): DIGIT = TABLE
    |v=1 OR w=1   | 1  ||
    |v=0 AND w=0  | 0  ||

When I generated the Latex, I get 

The problems:

(1) The first row does not have a vertical completion at the end?

(2) Why is there a first row (which is blank for this example)?

(3) Why is there so much space around the table?

(4) Why is the table offset to the left, rather than inline with TABLE and ENDTABLE?

Just wondered if I am doing something wrong?

Thanks and regards,