PVS icon indicating copy to clipboard operation
PVS copied to clipboard

latex rendering of tables is confused

Open kai-e opened this issue 3 years ago • 0 comments

I've tried two versions of table for gcd. Both render incorrectly.

gcd2(x,y): RECURSIVE posnat =
  TABLE
  %--------+-------------+-------------++
  |[ x = y | x > y       | ELSE        ]|
  %--------+-------------+-------------++
  | x      | gcd2(x-y,y) | gcd2(x,y-x) ||
  %--------+-------------+-------------++
  ENDTABLE
  MEASURE x+y

has an empty first cell. The one below it contains x.

gcd2(x,y): RECURSIVE posnat =
  TABLE
  %-------+-------------++
  | x = y | x           ||
  %-------+-------------++
  | x > y | gcd2(x-y,y) ||
  %-------+-------------++
  | ELSE  | gcd2(x,y-x) ||
  %-------+-------------++
  ENDTABLE
  MEASURE x+y

has an additional empty first line that ends "open".

kai-e avatar Nov 02 '21 01:11 kai-e