| changeset 6068 | 2d8f3e1f1151 |
| parent 3840 | e0baea4d485a |
| child 11318 | 6536fb8c9fc6 |
| 6067:0f8ab32093ae | 6068:2d8f3e1f1151 |
|---|---|
19 map_emp :: i |
19 map_emp :: i |
20 map_owr :: [i,i,i]=>i |
20 map_owr :: [i,i,i]=>i |
21 map_app :: [i,i]=>i |
21 map_app :: [i,i]=>i |
22 defs |
22 defs |
23 map_emp_def "map_emp == 0" |
23 map_emp_def "map_emp == 0" |
24 map_owr_def "map_owr(m,a,b) == SUM x:{a} Un domain(m).if(x=a,b,m``{x})" |
24 map_owr_def "map_owr(m,a,b) == |
25 SUM x:{a} Un domain(m). if x=a then b else m``{x}" |
|
25 map_app_def "map_app(m,a) == m``{a}" |
26 map_app_def "map_app(m,a) == m``{a}" |
26 |
27 |
27 end |
28 end |