SRI-CSL / PVS

The People's Verification System
http://pvs.csl.sri.com
GNU General Public License v2.0
132 stars 32 forks source link

latex rendering of tables is confused #85

Open kai-e opened 2 years ago

kai-e commented 2 years ago

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".