Changeset 1636 for src/utilities

Timestamp:

Jan 9, 2012, 12:38:32 PM (9 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:

• src/utilities/bindLists.ma (modified) (2 diffs)

src/utilities/bindLists.ma

@@ -67 +67 @@
  }.
  
-notation < "hvbox(νν ident l \nbsp 'of' \nbsp ts \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
+notation > "νν ident l : ty 'of' ts opt('with' ident EQ) 'in' f" with precedence 47 for
+ ${default
+   @{ 'stnews $ts (λ${ident l}:$ty.λ${ident EQ}.$f) }
+   @{ 'tnews $ts (λ${ident l}:$ty.$f)}
+ }.
+ 
+notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
    @{ 'stnews $ts (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
-notation < "hvbox(νν ident l \nbsp 'of' \nbsp ts \nbsp 'in'  break f)" with precedence 47 for
+notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'in'  break f)" with precedence 47 for
    @{ 'tnews $ts (λ${ident l} : $ty.$f) }.
 
-notation > "νν ident l : n opt('with' ident EQ) 'in' f" with precedence 47 for
+notation > "νν ident l × n opt('with' ident EQ) 'in' f" with precedence 47 for
  ${default
    @{ 'sunews $n (λ${ident l}.λ${ident EQ}.$f) }
@@ -78 +84 @@
  }.
  
-notation < "hvbox(νν ident l : n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
+notation > "νν ident l : ty × n opt('with' ident EQ) 'in' f" with precedence 47 for
+ ${default
+   @{ 'sunews $n (λ${ident l}:$ty.λ${ident EQ}.$f) }
+   @{ 'unews $n (λ${ident l}:$ty.$f)}
+ }.
+ 
+notation < "hvbox(νν \nbsp ident l : ty × n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
    @{ 'sunews $n (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
-notation < "hvbox(νν ident l : n \nbsp 'in' \nbsp break f)" with precedence 47 for
+notation < "hvbox(νν_ n \nbsp ident l : ty × n \nbsp 'in' \nbsp break f)" with precedence 47 for
    @{ 'unews $n (λ${ident l} : $ty.$f) }.