added cpp files
added rest files
changed typing rules
trying to prove tObjLoc, but found an error in efxmap=>output, now trying to rewrite it..
rewrote conversion.elf, also changed =
formatted clsmap2predmap.thm, minor change on conversion.elf
test.
test again.
in the process of proving tLit.
Changed conversion to produce different output for unique and
shared. Changed clsmap-cxt to only permit cxt with notnull
types.
proved two cases for ref-typing-ok/lit, but they
are not accepted by the checker.
only a definition for now..
proved lit.
added clauses for borrow in efxmap2output.
but not sure this is the correct way..
proved ref-typing-ok/lit*,
but as in conversion.elf, not sure need to
prove cases for borrow.
I intend to eliminate it completely later.
rewrote efxmap2output to changed the output permission
format, and also reduced the cases.
ready to rewrite proof for ref-typing-ok/lit*
changed (yet again) definition for efxmap2output.
*** empty log message ***
(re)proved ref-typing-ok/lit.