diff --git a/base/src/main/java/org/aya/tyck/tycker/StateBased.java b/base/src/main/java/org/aya/tyck/tycker/StateBased.java index 466cee6d..23c1fe00 100644 --- a/base/src/main/java/org/aya/tyck/tycker/StateBased.java +++ b/base/src/main/java/org/aya/tyck/tycker/StateBased.java @@ -37,7 +37,7 @@ public sealed interface StateBased permits AbstractExprTycker { default > @NotNull Result defCall(DefVar defVar, Callable.Factory function) { var tele = TeleDef.defTele(defVar); - var spine = tele.mapIndexed((i, type) -> type.map(_ -> new LocalTerm(tele.size() - 1 - i))); // λ. λ. λ. someCtor 2 1 0 + var spine = tele.mapIndexed((i, type) -> type.map(x -> new LocalTerm(tele.size() - 1 - i))); // λ. λ. λ. someCtor 2 1 0 Term body = function.make(defVar, 0, spine); var type = PiTerm.make(tele, TeleDef.defResult(defVar)); if ((defVar.core instanceof FnDef fn && fn.modifiers.contains(Modifier.Inline)) /*|| defVar.core instanceof PrimDef*/) { diff --git a/base/src/test/java/org/aya/syntax/core/BindTest.java b/base/src/test/java/org/aya/syntax/core/BindTest.java index 22f0b00a..da094580 100644 --- a/base/src/test/java/org/aya/syntax/core/BindTest.java +++ b/base/src/test/java/org/aya/syntax/core/BindTest.java @@ -29,19 +29,4 @@ public class BindTest { var expect = new LamTerm(true, new LamTerm(true, new AppTerm(new LocalTerm(1), Arg.ofExplicitly(new LocalTerm(0))))); assertEquals(expect, lamXYXY); } - - - @Test - public void tyckLam() { - var x = new LocalVar("x", SourcePos.NONE); - var y = new LocalVar("y", SourcePos.NONE); - // x y - var body = new Expr.App(new WithPos<>(SourcePos.NONE, new Expr.Ref(x)), new Expr.NamedArg(SourcePos.NONE, true, null, new WithPos<>(SourcePos.NONE, new Expr.Ref(y)))); - // λ y. x y - var lamYXY = new Expr.Lambda(new Expr.Param(SourcePos.NONE, y, true), new WithPos<>(SourcePos.NONE, body)); - var lamXYXY = new Expr.Lambda(new Expr.Param(SourcePos.NONE, x, true), new WithPos<>(SourcePos.NONE, lamYXY)); - var tycker = new ExprTycker(null, new LocalCtx(MutableMap.create(), null), null); - var result = tycker.synthesize(lamXYXY); - return; - } }