search

JetBrains / intellij-arend

Arend plugin for IntelliJ IDEA
Apache License 2.0
90 stars 12 forks source link

IllegalStateException in "Generate function from goal" intention #565

Open sxhya opened 4 weeks ago

sxhya commented 4 weeks ago

Replace the usage of simplify tactic in Module.*c_zro-left with {?}. Then call "Generate function from goal" intention on the goal.

java.lang.IllegalStateException: Minimization of expression (E) is likely diverged. Please report it to maintainers.
 Errors: 
[]
    at org.arend.term.prettyprint.MinimizedRepresentation.generateMinimizedRepresentation(MinimizedRepresentation.java:69)
    at org.arend.intention.AbstractGenerateFunctionIntention.getMinimizationPrettyPrinter$lambda$11(AbstractGenerateFunctionIntention.kt:185)
    at org.arend.intention.AbstractGenerateFunctionIntention.buildNewFunctionRepresentation$lambda$5(AbstractGenerateFunctionIntention.kt:138)
    at kotlin.text.StringsKt__AppendableKt.appendElement(Appendable.kt:84)
    at kotlin.collections.CollectionsKt___CollectionsKt.joinTo(_Collections.kt:3493)
    at kotlin.collections.CollectionsKt___CollectionsKt.joinToString(_Collections.kt:3510)
    at kotlin.collections.CollectionsKt___CollectionsKt.joinToString$default(_Collections.kt:3509)
    at org.arend.intention.AbstractGenerateFunctionIntention.buildNewFunctionRepresentation$intellij_arend(AbstractGenerateFunctionIntention.kt:136)
    at org.arend.intention.AbstractGenerateFunctionIntention.performRefactoring$intellij_arend(AbstractGenerateFunctionIntention.kt:98)
    at org.arend.intention.AbstractGenerateFunctionIntention.invoke(AbstractGenerateFunctionIntention.kt:87)
    at com.intellij.codeInsight.intention.impl.config.IntentionActionWrapper.invoke(IntentionActionWrapper.java:77)