Changeset 1636 for src/utilities


Ignore:
Timestamp:
Jan 9, 2012, 12:38:32 PM (8 years ago)
Author:
tranquil
Message:
  • added coercions to arguments (in RTL) and notation for ops (for the momenti in RTLabsToRTL)
  • changed slightly notations for bindLists
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/bindLists.ma

    r1635 r1636  
    6767 }.
    6868 
    69 notation < "hvbox(νν ident l \nbsp 'of' \nbsp ts \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
     69notation > "νν ident l : ty 'of' ts opt('with' ident EQ) 'in' f" with precedence 47 for
     70 ${default
     71   @{ 'stnews $ts (λ${ident l}:$ty.λ${ident EQ}.$f) }
     72   @{ 'tnews $ts (λ${ident l}:$ty.$f)}
     73 }.
     74 
     75notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
    7076   @{ 'stnews $ts (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
    71 notation < "hvbox(νν ident l \nbsp 'of' \nbsp ts \nbsp 'in'  break f)" with precedence 47 for
     77notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'in'  break f)" with precedence 47 for
    7278   @{ 'tnews $ts (λ${ident l} : $ty.$f) }.
    7379
    74 notation > "νν ident l : n opt('with' ident EQ) 'in' f" with precedence 47 for
     80notation > "νν ident l × n opt('with' ident EQ) 'in' f" with precedence 47 for
    7581 ${default
    7682   @{ 'sunews $n (λ${ident l}.λ${ident EQ}.$f) }
     
    7884 }.
    7985 
    80 notation < "hvbox(νν ident l : n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
     86notation > "νν ident l : ty × n opt('with' ident EQ) 'in' f" with precedence 47 for
     87 ${default
     88   @{ 'sunews $n (λ${ident l}:$ty.λ${ident EQ}.$f) }
     89   @{ 'unews $n (λ${ident l}:$ty.$f)}
     90 }.
     91 
     92notation < "hvbox(νν \nbsp ident l : ty × n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
    8193   @{ 'sunews $n (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
    82 notation < "hvbox(νν ident l : n \nbsp 'in' \nbsp break f)" with precedence 47 for
     94notation < "hvbox(νν_ n \nbsp ident l : ty × n \nbsp 'in' \nbsp break f)" with precedence 47 for
    8395   @{ 'unews $n (λ${ident l} : $ty.$f) }.
    8496
Note: See TracChangeset for help on using the changeset viewer.