DivisionFn |
appearance as argument number 1 |
![]() |
(documentation DivisionFn ChineseLanguage "如果 ?NUMBER1 和 ?NUMBER2 是 Number,那么 (DivisionFn ?NUMBER1 ?NUMBER2)就是 ?NUMBER1 除 ?NUMBER2 的商。注:当 ?NUMBER1 = 1 时, (DivisionFn ?NUMBER1 ?NUMBER2)就是 ?NUMBER2 的倒数。也要注意的是当 ?NUMBER2 = 0 时, (DivisionFn ?NUMBER1?NUMBER2) 会是为定义。") | chinese_format.kif 2220-2223 | |
(documentation DivisionFn EnglishLanguage "If ?NUMBER1 and ?NUMBER2 are Numbers, then (DivisionFn ?NUMBER1 ?NUMBER2) is the result of dividing ?NUMBER1 by ?NUMBER2. Note that when ?NUMBER1 = 1 (DivisionFn ?NUMBER1 ?NUMBER2) is the reciprocal of ?NUMBER2. Note too that (DivisionFn ?NUMBER1 ?NUMBER2) is undefined when ?NUMBER2 = 0.") | Merge.kif 4650-4654 | |
(domain DivisionFn 1 RealNumber) | Merge.kif 4646-4646 | The number 1 argument of division is an instance of real number |
(domain DivisionFn 2 RealNumber) | Merge.kif 4647-4647 | The number 2 argument of division is an instance of real number |
(identityElement DivisionFn 1) | Merge.kif 5197-5197 | 1 is an identity element of division |
(instance DivisionFn BinaryFunction) | Merge.kif 4643-4643 | Division is an instance of binary function |
(instance DivisionFn PartialValuedRelation) | Merge.kif 4645-4645 | Division is an instance of partial valued relation |
(range DivisionFn RealNumber) | Merge.kif 4648-4648 | The range of division is an instance of real number |
appearance as argument number 2 |
![]() |
(format ChineseLanguage DivisionFn "%*[/]") | chinese_format.kif 686-686 | |
(format EnglishLanguage DivisionFn "%*[/]") | english_format.kif 688-688 | |
(termFormat ChineseLanguage DivisionFn "部") | domainEnglishFormat.kif 19983-19983 | |
(termFormat ChineseLanguage DivisionFn "除法函数") | chinese_format.kif 687-687 | |
(termFormat ChineseTraditionalLanguage DivisionFn "部") | domainEnglishFormat.kif 19982-19982 | |
(termFormat EnglishLanguage DivisionFn "division") | domainEnglishFormat.kif 19981-19981 |
antecedent |
![]() |
consequent |
![]() |
statement |
![]() |
![]() |
![]() |