in src/main/kotlin/org/arend/quickfix/ImplementMissingClausesQuickFix.kt [254:270]
fun getIntegralNumber(pattern: CorePattern): Int? {
val definition = pattern.constructor
val isSuc = definition == Prelude.SUC
val isFinSuc = definition == Prelude.FIN_SUC
val isPos = definition == Prelude.POS
val isNeg = definition == Prelude.NEG
val firstArgument = (pattern as? ConstructorExpressionPattern)?.dataTypeArguments?.firstOrNull()
if (isSuc || isFinSuc || isPos || isNeg) {
val number = if (isFinSuc && (firstArgument as? SmallIntegerExpression)?.isOne == true) 0 else
getIntegralNumber(pattern.subPatterns.firstOrNull() ?: return null)
if ((isSuc || isFinSuc) && number != null) return number + 1
if (isPos && number != null) return number
if (isNeg && number != null && number != 0) return -number
return null
} else if (definition == Prelude.ZERO || definition == Prelude.FIN_ZERO) return 0
return null
}