模块 aya.guest.base

程序包 org.aya.guest0x0.tyck

接口 HCompPDF

public interface HCompPDF

References:

• 10_value_fibrant.scala
• hcomp.pdf

嵌套类概要

嵌套类

修饰符和类型	接口	说明
static final record	HCompPDF.Transps

方法概要

静态方法

修饰符和类型	方法	说明
static @NotNull Term	comp(@NotNull Term cover, @NotNull LocalVar x, @NotNull org.aya.guest0x0.cubical.Partial<Term> par, @NotNull Term u0)	CCHM comp, similar to the analogous comp as in mlang
static @NotNull Term	forward(@NotNull Term cover, @NotNull Term r)

方法详细资料

forward

@NotNull
static @NotNull Term forward(@NotNull
 @NotNull Term cover,
 @NotNull
 @NotNull Term r)

comp

@NotNull
static @NotNull Term comp(@NotNull
 @NotNull Term cover,
 @NotNull
 @NotNull LocalVar x,
 @NotNull
 @NotNull org.aya.guest0x0.cubical.Partial<Term> par,
 @NotNull
 @NotNull Term u0)

CCHM comp, similar to the analogous comp as in mlang

参数:

x - the wall dimension

par - has access to x