override fun getExternalParameters()

in src/main/kotlin/org/arend/psi/ext/ArendDefinition.kt [80:104]


    override fun getExternalParameters(): List<ParameterReferable> {
        val parent = locatedReferableParent as? ArendDefinition<*> ?: return emptyList()
        val tcRef = parent.tcReferable as? TCDefReferable ?: return emptyList()
        val params = parent.parametersExt
        if (params.isEmpty()) return emptyList()

        val eliminated = if (parent is Abstract.FunctionDefinition && !parent.withTerm() && !parent.isCowith) {
            val elimList = parent.eliminatedExpressions
            if (elimList.isEmpty()) return emptyList()
            elimList.mapTo(HashSet()) { it.referent.refName }
        } else emptySet()

        val result = ArrayList<ParameterReferable>()
        var i = 0
        for (param in params) {
            val classRef = (param.type as? ArendExpr)?.let { ReferableExtractVisitor().findClassReferable(it) }
            for (referable in param.referableList) {
                if (referable != null && !eliminated.contains(referable.refName)) {
                    result.add(ParameterReferable(tcRef, i, referable, if (classRef == null) null else Concrete.ReferenceExpression(null, classRef)))
                }
                i++
            }
        }
        return result
    }