Skip to content

Commit

Permalink
test: do not test too complicated case yet
Browse files Browse the repository at this point in the history
  • Loading branch information
ice1000 committed Jan 20, 2025
1 parent 79c8c44 commit 330ff17
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 4 deletions.
2 changes: 1 addition & 1 deletion base/src/main/java/org/aya/resolve/salt/Desalt.java
Original file line number Diff line number Diff line change
Expand Up @@ -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
));
}
Expand Down
9 changes: 6 additions & 3 deletions cli-impl/src/test/resources/success/src/Test.aya
Original file line number Diff line number Diff line change
Expand Up @@ -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 }

0 comments on commit 330ff17

Please sign in to comment.