模块 aya.guest.base

程序包 org.aya.guest0x0.syntax

Record Class Expr.SubEl

java.lang.Object

java.lang.Record

org.aya.guest0x0.syntax.Expr.SubEl

记录组件：

isIntro - true if inS

所有已实现的接口:

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

封闭接口:

Expr

public static record Expr.SubEl(@NotNull org.aya.util.error.SourcePos pos, @NotNull Expr e, boolean isIntro)
extends Record
implements Expr

inS/outS, the introduction/elimination rules for the subtype relation

嵌套类概要

从接口继承的嵌套类/接口 org.aya.guest0x0.syntax.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

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

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

构造器概要

构造器

构造器	说明
SubEl(@NotNull org.aya.util.error.SourcePos pos, @NotNull Expr e, boolean isIntro)	创建 SubEl 记录的实例。

方法概要

修饰符和类型	方法	说明
@NotNull Expr	e()	返回 e 记录组件的值。
final boolean	equals(Object o)	指示某个其他对象是否“等于”此对象。
final int	hashCode()	返回此对象的哈希代码值。
boolean	isIntro()	返回 isIntro 记录组件的值。
@NotNull org.aya.util.error.SourcePos	pos()	返回 pos 记录组件的值。
final String	toString()	返回此记录的字符串表示形式。

从类继承的方法 java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

从接口继承的方法 org.aya.guest0x0.syntax.Expr

toDoc

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

asFormula

构造器详细资料

SubEl

public SubEl(@NotNull
 @NotNull org.aya.util.error.SourcePos pos,
 @NotNull
 @NotNull Expr e,
 boolean isIntro)

创建 SubEl 记录的实例。

参数:

pos - pos 记录组件的值

e - e 记录组件的值

isIntro - isIntro 记录组件的值

方法详细资料

toString

public final String toString()

返回此记录的字符串表示形式。此表示形式包含类型的名称，后跟每个记录组件的名称和值。

指定者:

toString 在类中 Record

返回:

此对象的字符串表示形式

hashCode

public final int hashCode()

返回此对象的哈希代码值。此值派生自每个记录组件的哈希代码。

指定者:

hashCode 在类中 Record

返回:

此对象的哈希代码值

equals

public final boolean equals(Object o)

指示某个其他对象是否“等于”此对象。如果两个对象属于同一个类，而且所有记录组件都相等，则这两个对象相等。 使用 Objects::equals(Object,Object) 对参考组件进行比较；使用 '==' 对基元组件进行比较

指定者:

equals 在类中 Record

参数:

o - 要与之进行比较的对象

返回:

如果此对象与 o 参数相同，则为 true；否则为 false。

pos

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

返回 pos 记录组件的值。

指定者:

pos 在接口中 Expr

返回:

pos 记录组件的值

e

@NotNull
public @NotNull Expr e()

返回 e 记录组件的值。

返回:

e 记录组件的值

isIntro

public boolean isIntro()

返回 isIntro 记录组件的值。

返回:

isIntro 记录组件的值