From 330ff1721c442f6f8060916d5afaa1c87a5362fd Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Mon, 20 Jan 2025 03:53:50 -0500
Subject: [PATCH] test: do not test too complicated case yet

---
 base/src/main/java/org/aya/resolve/salt/Desalt.java | 2 +-
 cli-impl/src/test/resources/success/src/Test.aya    | 9 ++++++---
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/base/src/main/java/org/aya/resolve/salt/Desalt.java b/base/src/main/java/org/aya/resolve/salt/Desalt.java
index 820e42a10..ac26e76c8 100644
--- a/base/src/main/java/org/aya/resolve/salt/Desalt.java
+++ b/base/src/main/java/org/aya/resolve/salt/Desalt.java
@@ -100,7 +100,7 @@ public final class Desalt implements PosedUnaryOperator<Expr> {
             lamTele.map(x -> new WithPos<>(x.definition(), new Expr.Ref(x))),
             ImmutableSeq.of(lam.clause()),
             ImmutableSeq.empty(),
-            false,
+            true,
             null
           ));
         }
diff --git a/cli-impl/src/test/resources/success/src/Test.aya b/cli-impl/src/test/resources/success/src/Test.aya
index 309da5bd8..0972efe01 100644
--- a/cli-impl/src/test/resources/success/src/Test.aya
+++ b/cli-impl/src/test/resources/success/src/Test.aya
@@ -107,8 +107,11 @@ module Issue1249 {
 }
 
 module Issue94 {
-  open inductive IsZero Nat
-  | zero => ack
   def absurd (A : Type) : Empty -> A => fn ()
-  def irrefutable : Fn (a : Nat) -> IsZero a -> Nat => fn { zero, ack => 233 }
+  def obvious : Fn (a : Sig Nat ** Nat) -> Nat => fn { (a, b) => a + b }
 }
+
+// relies on match elim
+// open inductive IsZero Nat
+// | zero => ack
+// def irrefutable : Fn (a : Nat) -> IsZero a -> Nat => fn { zero, ack => 233 }