more!

base/src/main/java/org/aya/syntax/core/Signature.java

@@ -0,0 +1,25 @@
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.syntax.core;
+
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.generic.AyaDocile;
+import org.aya.pretty.doc.Doc;
+import org.aya.syntax.core.term.Term;
+import org.aya.util.Arg;
+import org.aya.util.prettier.PrettierOptions;
+import org.jetbrains.annotations.NotNull;
+
+/**
+ * Signature of a definition, used in concrete and tycking.
+ *
+ * @author ice1000
+ */
+public record Signature<T extends Term>(
+  @NotNull ImmutableSeq<Arg<Term>> param,
+  @NotNull T result
+) implements AyaDocile {
+  @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
+    // return Doc.sep(Doc.sep(param.view().map(p -> p.toDoc(options))), Doc.symbol("->"), result.toDoc(options));
+  }
+}

base/src/main/java/org/aya/syntax/ref/DefVar.java

@@ -1,16 +1,16 @@
 package org.aya.syntax.ref;
 
 import kala.collection.immutable.ImmutableSeq;
-import org.aya.syntax.concrete.decl.Decl;
-import org.aya.syntax.core.def.Def;
+import org.aya.syntax.concrete.stmt.decl.Decl;
+import org.aya.syntax.core.def.TeleDef;
 import org.aya.util.binop.Assoc;
 import org.aya.util.binop.OpDecl;
 import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 import org.jetbrains.annotations.UnknownNullability;
 
-public final class DefVar<Core extends Def, Concrete extends Decl> implements AnyVar {
+public final class DefVar<Core extends TeleDef, Concrete extends Decl> implements AnyVar {
   private final @NotNull String name;
   /** Initialized in parsing, so it might be null for deserialized user definitions. */
   public @UnknownNullability Concrete concrete;
@@ -39,13 +39,13 @@ private DefVar(Concrete concrete, Core core, @NotNull String name) {
   }
 
   /** Used in user definitions. */
-  public static <Core extends Def, Concrete extends Decl>
+  public static <Core extends TeleDef, Concrete extends Decl>
   @NotNull DefVar<Core, Concrete> concrete(@NotNull Concrete concrete, @NotNull String name) {
     return new DefVar<>(concrete, null, name);
   }
 
   /** Used in the serialization of core and primitive definitions. */
-  public static <Core extends Def, Concrete extends Decl>
+  public static <Core extends TeleDef, Concrete extends Decl>
   @NotNull DefVar<Core, Concrete> empty(@NotNull String name) {
     return new DefVar<>(null, null, name);
   }

base/src/main/java/org/aya/syntax/ref/LocalVar.java

@@ -5,6 +5,12 @@
 import org.jetbrains.annotations.Nullable;
 
 public record LocalVar(@NotNull String name, @NotNull SourcePos definition) {
+  public LocalVar(@NotNull String name) {
+    this(name, SourcePos.NONE);
+  }
+
+  public static final @NotNull LocalVar IGNORED = new LocalVar("_", SourcePos.NONE);
+
   @Override public boolean equals(@Nullable Object o) {
     return this == o;
   }