Changes between Version 5 and Version 6 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 5, 2006 7:52:28 AM (7 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}}}