mirror of https://github.com/davisking/dlib.git
Clarified spec.
--HG-- extra : convert_revision : svn%3Afdd8eb12-d10e-0410-9acb-85c331704f74/trunk%404178
This commit is contained in:
parent
02ec16db94
commit
f1d98591a8
|
@ -270,7 +270,7 @@ namespace dlib
|
|||
- is_vector(dest) == true
|
||||
- max_index_plus_one(src) <= dest.size()
|
||||
ensures
|
||||
- dest += C*src
|
||||
- #dest == dest + C*src
|
||||
!*/
|
||||
|
||||
// ----------------------------------------------------------------------------------------
|
||||
|
@ -287,7 +287,7 @@ namespace dlib
|
|||
- is_vector(dest) == true
|
||||
- max_index_plus_one(src) <= dest.size()
|
||||
ensures
|
||||
- dest -= C*src
|
||||
- #dest == dest - C*src
|
||||
!*/
|
||||
|
||||
// ----------------------------------------------------------------------------------------
|
||||
|
|
Loading…
Reference in New Issue