Changeset 1908 for src/utilities
 Timestamp:
 Apr 26, 2012, 5:38:07 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/proper.ma
r1640 r1908 13 13 interpretation "proper contravariant" 'proper_contra r s = (proper_contra ? ? r s). 14 14 15 notation "r ++> s" right associative with precedence 5 1for15 notation "r ++> s" right associative with precedence 56 for 16 16 @{'proper $r $s}. 17 17 18 notation "r +> s" right associative with precedence 5 1for18 notation "r +> s" right associative with precedence 56 for 19 19 @{'proper_contra $r $s}. 20 20 21 21 (* avoid notation from kikcing in in outputm to avoid things like X ⊨ Prod *) 22 notation > "f ⊨ p " with precedence 5 0for @{$p $f $f}.22 notation > "f ⊨ p " with precedence 55 for @{$p $f $f}.
Note: See TracChangeset
for help on using the changeset viewer.