next up previous contents
Next: Logical and Programming Style Up: Mark2 Prover Documentation Previous: Views and Theorem Export

Places where bugs are likely to be found

The theorem export facility is very complex and has not been tested under all possible perverse conditions; it is likely to be reliable but not perfectly reliable. Problems I am aware of involve the treatment of numerals!

The variable binding context is a new addition (originally, the bracket construction was used only for constant functions and there were no bound variables at all). I suspect it of having bugs, and I also suspect that I will find awkwardnesses in it which will require me to revise it somewhat.

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997