Changeset 1636 for src/utilities/bindLists.ma
 Timestamp:
 Jan 9, 2012, 12:38:32 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/bindLists.ma
r1635 r1636 67 67 }. 68 68 69 notation < "hvbox(νν ident l \nbsp 'of' \nbsp ts \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for 69 notation > "νν 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 75 notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for 70 76 @{ '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 for77 notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'in' break f)" with precedence 47 for 72 78 @{ 'tnews $ts (λ${ident l} : $ty.$f) }. 73 79 74 notation > "νν ident l :n opt('with' ident EQ) 'in' f" with precedence 47 for80 notation > "νν ident l × n opt('with' ident EQ) 'in' f" with precedence 47 for 75 81 ${default 76 82 @{ 'sunews $n (λ${ident l}.λ${ident EQ}.$f) } … … 78 84 }. 79 85 80 notation < "hvbox(νν ident l : n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for 86 notation > "νν 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 92 notation < "hvbox(νν \nbsp ident l : ty × n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for 81 93 @{ 'sunews $n (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }. 82 notation < "hvbox(νν ident l :n \nbsp 'in' \nbsp break f)" with precedence 47 for94 notation < "hvbox(νν_ n \nbsp ident l : ty × n \nbsp 'in' \nbsp break f)" with precedence 47 for 83 95 @{ 'unews $n (λ${ident l} : $ty.$f) }. 84 96
Note: See TracChangeset
for help on using the changeset viewer.