Changes between Version 5 and Version 6 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 5, 2006 7:52:28 AM (9 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC

    v5 v6  
    426426The literate implication constraints generated out of the
    427427program text may look as follows
    428 {{{ a=T Int implies ( a= S Int implies ...)
     428{{{
     429a=T Int implies ( a= S Int implies ...)
    429430}}}
    430431
    431432The above can be simplified to
    432 {{{ (a=T Int /\ a = S Int) implies ...}}}
     433{{{
     434(a=T Int /\ a = S Int) implies ...
     435}}}
    433436Before we proceed with the completion method, we first
    434437need to apply some closure rules (eg. transitivity, left, right etc)
    435438Hence, from the above we generatet
    436 {{{a=T Int /\ a = S Int /\
     439{{{
     440   a=T Int /\ a = S Int /\
    437441   T Int = a /\ S Int = a /\       -- symmetry
    438442   T Int = S Int /\ S Int = T Int  -- transitivity
    439443}}}
    440444We omit the trival (reflexive) equations
    441 {{{ T Int = T Int /\ S Int = S Int }}}
     445{{{
     446T Int = T Int /\ S Int = S Int
     447}}}