equal
deleted
inserted
replaced
40 id :: 'a => 'a |
40 id :: 'a => 'a |
41 "id == %x. x" |
41 "id == %x. x" |
42 |
42 |
43 o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55) |
43 o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55) |
44 "f o g == %x. f(g(x))" |
44 "f o g == %x. f(g(x))" |
45 |
45 |
46 inv :: ('a => 'b) => ('b => 'a) |
46 inv :: ('a => 'b) => ('b => 'a) |
47 "inv(f::'a=>'b) == % y. @x. f(x)=y" |
47 "inv(f::'a=>'b) == % y. @x. f(x)=y" |
48 |
48 |
49 inj_on :: ['a => 'b, 'a set] => bool |
49 inj_on :: ['a => 'b, 'a set] => bool |
50 "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" |
50 "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" |