 | 11.9 Names |
| 
| 11 PVS translator |
| |
| 11.10 Identifiers |
11.10 Identifiers
RSL allows primes on identifiers, but PVS does not. Primes translate
to the string rsL.
It is the user's responsibility to ensure that this translation does
not cause name clashes in PVS.
It is also the user's responsibility
to ensure that RSL identifiers do not clash with PVS reserved words.
These are not case sensitive, unlike the user defined identifiers in
PVS. So, for example, Lemma, lemma, and LEMMA would all clash with
LEMMA.
Chris George, April 17, 2008
| 11.10 Identifiers |
| 11.9 Names |
| |
| 11 PVS translator |
| |