ListSumFn |
appearance as argument number 1 |
(documentation ListSumFn EnglishLanguage "The sum of all the numbers in a List.") | Merge.kif 3243-3243 | |
(domain ListSumFn 1 List) | Merge.kif 3241-3241 | The number 1 argument of sum of elements is an instance of list |
(instance ListSumFn UnaryFunction) | Merge.kif 3240-3240 | Sum of elements is an instance of unary function |
(range ListSumFn RealNumber) | Merge.kif 3242-3242 | The range of sum of elements is an instance of real number |
appearance as argument number 2 |
(format EnglishLanguage ListSumFn "the sum of %1") | Merge.kif 3244-3244 | |
(termFormat EnglishLanguage ListSumFn "sum of elements") | Merge.kif 3245-3245 |
antecedent |
(=> (and (equal ?A (ListSumFn ?L)) (equal 1 (ListLengthFn ?L))) (equal ?A (ListOrderFn ?L 1))) |
Merge.kif 3253-3257 | |
(=> (and (equal ?A (ListSumFn ?L)) (greaterThan (ListLengthFn ?L) 1)) (equal ?A (AdditionFn (FirstFn ?L) (ListSumFn (SubListFn 2 (ListLengthFn ?L) ?L))))) |
Merge.kif 3259-3269 |
consequent |