source: src/utilities/proper.ma @ 2200

Last change on this file since 2200 was 1908, checked in by fguidi, 8 years ago

notation fixup following last commit of matita
we shifted the levels of precedence from 50 to 60 up by 5

File size: 756 bytes
RevLine 
[1635]1include "basics/relations.ma".
2
3definition proper ≝ λA,B.λrelA : relation A.λrelB : relation B.
4λf,g : A → B.
5  ∀a,a' : A.relA a a' → relB (f a) (g a').
6
7definition proper_contra ≝ λA,B.λrelA : relation A.λrelB : relation B.
8λf,g : A → B.
9  ∀a,a' : A.relA a' a → relB (f a) (g a').
10
11
12interpretation "proper" 'proper r s = (proper ? ? r s).
13interpretation "proper contravariant" 'proper_contra r s = (proper_contra ? ? r s).
14
[1908]15notation "r ++> s" right associative with precedence 56 for
[1635]16  @{'proper $r $s}.
17
[1908]18notation "r -+> s" right associative with precedence 56 for
[1635]19  @{'proper_contra $r $s}.
20
[1640]21(* avoid notation from kikcing in in outputm to avoid things like X ⊨ Prod *)
[1908]22notation > "f ⊨ p " with precedence 55 for @{$p $f $f}.
Note: See TracBrowser for help on using the repository browser.