ListSumFn |
appearance as argument number 1 |
(documentation ListSumFn EnglishLanguage "The sum of all the numbers in a List.") | Merge.kif 3242-3242 | |
(domain ListSumFn 1 List) | Merge.kif 3240-3240 | 域 ListSumFn, 1 and List |
(instance ListSumFn UnaryFunction) | Merge.kif 3239-3239 | 例 ListSumFn and UnaryFunction |
(range ListSumFn RealNumber) | Merge.kif 3241-3241 | 範圍 ListSumFn and RealNumber |
appearance as argument number 2 |
(format EnglishLanguage ListSumFn "the sum of %1") | Merge.kif 3243-3243 | |
(termFormat EnglishLanguage ListSumFn "sum of elements") | Merge.kif 3244-3244 |
antecedent |
(=> (and (equal ?A (ListSumFn ?L)) (equal 1 (ListLengthFn ?L))) (equal ?A (ListOrderFn ?L 1))) |
Merge.kif 3252-3256 | |
(=> (and (equal ?A (ListSumFn ?L)) (greaterThan (ListLengthFn ?L) 1)) (equal ?A (AdditionFn (FirstFn ?L) (ListSumFn (SubListFn 2 (ListLengthFn ?L) ?L))))) |
Merge.kif 3258-3268 |
consequent |
(=> (and (amount ?S ?CO (MeasureFn ?N ?U)) (instance ?SI ?S) (measure ?SI (MeasureFn ?N2 ?U)) (part ?SI ?CO)) (exists (?L) (and (inList (MeasureFn ?N2 ?U) ?L) (equal ?L (AmountsFn ?S ?CO ?U)) (equal ?N (ListSumFn ?L))))) |
Merge.kif 7596-7611 |
|
(=> (and (equal ?A (AverageFn ?L)) (greaterThan (ListLengthFn ?L) 0)) (equal ?A (DivisionFn (ListSumFn ?L) (ListLengthFn ?L)))) |
Merge.kif 3277-3284 | |
(=> (and (equal ?A (ListSumFn ?L)) (greaterThan (ListLengthFn ?L) 1)) (equal ?A (AdditionFn (FirstFn ?L) (ListSumFn (SubListFn 2 (ListLengthFn ?L) ?L))))) |
Merge.kif 3258-3268 |