Refactor metric spaces

JetBrains · Oct 4, 2024 · 86aaf0d · 86aaf0d
1 parent 4bee850
commit 86aaf0d
Showing 1 changed file with 9 additions and 1 deletion.
diff --git a/base/src/main/java/org/arend/core/expr/visitor/CompareVisitor.java b/base/src/main/java/org/arend/core/expr/visitor/CompareVisitor.java
@@ -1142,7 +1142,15 @@ private Boolean checkDefCallAndApp(Expression expr1, Expression expr2, boolean c
  TypeClassInferenceVariable variable;
  FieldCallExpression fieldCall = funNorm.cast(FieldCallExpression.class);
  if (fieldCall != null) {
- InferenceVariable infVar = fieldCall.getArgument().getInferenceVariable();
+ while (true) {
+ funNorm = myNormalCompare ? fieldCall.getArgument().normalize(NormalizationMode.WHNF) : fieldCall.getArgument();
+ if (funNorm instanceof FieldCallExpression) {
+ fieldCall = (FieldCallExpression) funNorm;
+ } else {
+ break;
+ }
+ }
+ InferenceVariable infVar = funNorm.getInferenceVariable();
  variable = infVar instanceof TypeClassInferenceVariable ? (TypeClassInferenceVariable) infVar : null;
  } else {
  variable = null;