模块 aya.guest.base

程序包 org.aya.guest0x0.syntax

接口 Expr

所有超级接口:

org.aya.pretty.doc.Docile, org.aya.guest0x0.cubical.Restr.TermLike<Expr>

所有已知实现类:

Expr.Cof, Expr.DT, Expr.Hcomp, Expr.Hole, Expr.Lam, Expr.Mula, Expr.PartEl, Expr.PartTy, Expr.Path, Expr.PrimTy, Expr.Proj, Expr.Resolved, Expr.Sub, Expr.SubEl, Expr.Transp, Expr.Two, Expr.Unresolved

public sealed interface Expr
extends org.aya.pretty.doc.Docile, org.aya.guest0x0.cubical.Restr.TermLike<Expr>
permits Expr.Unresolved, Expr.Resolved, Expr.Two, Expr.Lam, Expr.Proj, Expr.PrimTy, Expr.Hole, Expr.DT, Expr.Path, Expr.Mula, Expr.Transp, Expr.Cof, Expr.PartEl, Expr.PartTy, Expr.Sub, Expr.SubEl, Expr.Hcomp

嵌套类概要

嵌套类

修饰符和类型	接口	说明
static final record	Expr.Cof
static final record	Expr.DT
static final record	Expr.Hcomp
static final record	Expr.Hole
static final record	Expr.Lam
static final record	Expr.Mula
static final record	Expr.PartEl
static final record	Expr.PartTy
static final record	Expr.Path
static final record	Expr.PrimTy
static final record	Expr.Proj
static final record	Expr.Resolved
static final record	Expr.Sub	"Proper" cubical subtypes
static final record	Expr.SubEl	inS/outS, the introduction/elimination rules for the subtype relation
static final record	Expr.Transp
static final record	Expr.Two
static final record	Expr.Unresolved

从接口继承的嵌套类/接口 org.aya.guest0x0.cubical.Restr.TermLike

org.aya.guest0x0.cubical.Restr.TermLike.Factory<T extends Object>

方法概要

修饰符和类型	方法	说明
@NotNull org.aya.util.error.SourcePos	pos()
default @NotNull org.aya.pretty.doc.Doc	toDoc()
static @Nullable Expr	unlam(kala.collection.mutable.MutableList<LocalVar> binds, int n, Expr body)

从接口继承的方法 org.aya.guest0x0.cubical.Restr.TermLike

asFormula

方法详细资料

pos

@NotNull
@NotNull org.aya.util.error.SourcePos pos()

toDoc

@NotNull
default @NotNull org.aya.pretty.doc.Doc toDoc()

指定者:

toDoc 在接口中 org.aya.pretty.doc.Docile

unlam

@Nullable
static @Nullable Expr unlam(kala.collection.mutable.MutableList<LocalVar> binds,
 int n,
 Expr body)