Changes between Version 3 and Version 4 of TypeNats/Interact1


Ignore:
Timestamp:
Dec 15, 2010 6:08:38 PM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Interact1

    v3 v4  
    1212Top-level interactions for <= 
    1313{{{ 
    14 m <= n   <=> {m <= n} = True 
     14m <= n   <=> {m <= n} 
    15150 <= a   <=> True 
    1616a <= 0   <=> a ~ 0 
     
    1919Top-level interactions for +. 
    2020{{{ 
    21 (m + n ~ k) <=> {m + n} = k 
     21(m + n ~ k) <=> {m + n} == k 
    2222(m + a ~ n) <=> a ~ {n - m}    -- n >= m 
    2323(a + m ~ n) <=> a ~ {n - m}    -- n >= m 
     
    3232Top-level interactions for *. 
    3333{{{ 
    34 (m * n ~ k) <=> {m * n} = k 
     34(m * n ~ k) <=> {m * n} == k 
    3535(m * a ~ n) <=> a ~ {n / m}     -- m `divides` n 
    3636(a * m ~ n) <=> a ~ {n / m}     -- m `divides` n 
     
    4545Top-level interactions for {{{^}}} 
    4646{{{ 
    47 (m ^ n ~ k) <=> {m ^ n} = k 
     47(m ^ n ~ k) <=> {m ^ n} == k 
    4848(m ^ a ~ n) <=> a ~ {log m n}   -- log (base m) of n exists 
    4949(a ^ m ~ n) <=> a ~ {root m n}  -- m-th root of n exists