From 7c01dacfd2e06be70b94035b16480517e1a7acab Mon Sep 17 00:00:00 2001 From: ice1000 Date: Fri, 6 Jan 2023 19:32:41 -0500 Subject: [PATCH] subst: always use a linked map --- base/src/main/java/org/aya/core/visitor/Subst.java | 2 +- base/src/test/resources/failure/holes/issue747.aya.txt | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/base/src/main/java/org/aya/core/visitor/Subst.java b/base/src/main/java/org/aya/core/visitor/Subst.java index 49fd5c6604..9cedb76b47 100644 --- a/base/src/main/java/org/aya/core/visitor/Subst.java +++ b/base/src/main/java/org/aya/core/visitor/Subst.java @@ -42,7 +42,7 @@ public record Subst( })); public Subst() { - this(MutableMap.create()); + this(MutableLinkedHashMap.of()); } public Subst(@NotNull AnyVar var, @NotNull Term term) { diff --git a/base/src/test/resources/failure/holes/issue747.aya.txt b/base/src/test/resources/failure/holes/issue747.aya.txt index c6518135ef..c189d603ab 100644 --- a/base/src/test/resources/failure/holes/issue747.aya.txt +++ b/base/src/test/resources/failure/holes/issue747.aya.txt @@ -11,7 +11,7 @@ Goal: Goal of type Context: {a : Nat} To ensure confluence: - Given (_ ⇒ 0, i ⇒ _), we should have: 0 + Given (i ⇒ _, _ ⇒ 0), we should have: 0 In file $FILE:11:13 ->