模块 aya.guest.base
程序包 org.aya.guest0x0.syntax

接口 Term

所有超级接口:
org.aya.pretty.doc.Docile, org.aya.guest0x0.cubical.Restr.TermLike<Term>
所有已知实现类:
Term.Call, Term.Cof, Term.DT, Term.Hcomp, Term.InS, Term.Lam, Term.Mula, Term.OutS, Term.PartEl, Term.PartTy, Term.Path, Term.PCall, Term.PLam, Term.Proj, Term.Ref, Term.Sub, Term.Transp, Term.Two, Term.UI
public sealed interface Term extends org.aya.pretty.doc.Docile, org.aya.guest0x0.cubical.Restr.TermLike<Term> permits Term.Lam, Term.Ref, Term.Call, Term.Two, Term.Proj, Term.DT, Term.UI, Term.Path, Term.PLam, Term.PCall, Term.Mula, Term.Transp, Term.Cof, Term.PartTy, Term.PartEl, Term.Sub, Term.InS, Term.OutS, Term.Hcomp

  • 嵌套类概要

    嵌套类
    修饰符和类型
    接口
    说明
    static final record 
    Term.Call
     
    static final record 
    Term.Cof
     
    static final record 
    Term.DT
     
    static final record 
    Term.Hcomp
     
    static final record 
    Term.InS
     
    static final record 
    Term.Lam
     
    static final record 
    Term.Mula
     
    static final record 
    Term.OutS
     
    static final record 
    Term.PartEl
     
    static final record 
    Term.PartTy
     
    static final record 
    Term.Path
     
    static final record 
    Term.PCall
     
    static final record 
    Term.PLam
     
    static final record 
    Term.Proj
     
    static final record 
    Term.Ref
     
    static final record 
    Term.Sub
     
    static final record 
    Term.Transp
     
    static final record 
    Term.Two
     
    static final record 
    Term.UI
     

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

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

  • 字段概要

    字段
    修饰符和类型
    字段
    说明
    static final @NotNull Term
    F
     
    static final @NotNull Term
    I
     
    static final @NotNull Term
    U
     

  • 方法概要

    修饰符和类型
    方法
    说明
    static @NotNull Term
    and(@NotNull Term l, @NotNull Term r)
     
    default @NotNull Term
    app(@NotNull Term... args)
     
    static @NotNull Term
    conn(boolean isAnd, @NotNull Term l, @NotNull Term r)
     
    static @NotNull Term
    end(boolean isLeft)
     
    static @NotNull Term.Lam
    id(@NotNull String x)
     
    static @NotNull Term.Lam
    mkLam(@NotNull String x, @NotNull Function<Term,Term> body)
     
    static @NotNull Term
    mkLam(@NotNull kala.collection.SeqView<LocalVar> telescope, @NotNull Term body)
     
    static @NotNull Term
    mkPi(@NotNull kala.collection.immutable.ImmutableSeq<Param<Term>> telescope, @NotNull Term body)
     
    static @NotNull Term
    mkPi(@NotNull Term dom, @NotNull Term cod)
     
    static @NotNull Term
    neg(@NotNull Term term)
     
    static @NotNull Term
    or(@NotNull Term l, @NotNull Term r)
     
    default @NotNull Term
    proj(boolean isOne)
     
    default @NotNull Term
    subst(@NotNull kala.collection.mutable.MutableMap<LocalVar,Term> map)
     
    default @NotNull Term
    subst(@NotNull LocalVar x, @NotNull Term t)
     
    default @NotNull org.aya.pretty.doc.Doc
    toDoc()
     
    static @Nullable Term
    unlam(kala.collection.mutable.MutableList<LocalVar> binds, Term t, int n)
     
    static @Nullable Term
    unpi(kala.collection.mutable.MutableList<LocalVar> binds, Term t, int n)
     

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

    asFormula

  • 字段详细资料

    • U

      @NotNull static final @NotNull Term U

    • I

      @NotNull static final @NotNull Term I

    • F

      @NotNull static final @NotNull Term F

  • 方法详细资料

    • toDoc

      @NotNull default @NotNull org.aya.pretty.doc.Doc toDoc()
      指定者:
      toDoc 在接口中 org.aya.pretty.doc.Docile

    • subst

      @NotNull default @NotNull Term subst(@NotNull @NotNull LocalVar x, @NotNull @NotNull Term t)

    • subst

      @NotNull default @NotNull Term subst(@NotNull @NotNull kala.collection.mutable.MutableMap<LocalVar,Term> map)

    • unlam

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

    • unpi

      @Nullable static @Nullable Term unpi(kala.collection.mutable.MutableList<LocalVar> binds, Term t, int n)

    • mkLam

      @NotNull static @NotNull Term mkLam(@NotNull @NotNull kala.collection.SeqView<LocalVar> telescope, @NotNull @NotNull Term body)

    • id

      @NotNull static @NotNull Term.Lam id(@NotNull @NotNull String x)

    • mkLam

      @NotNull static @NotNull Term.Lam mkLam(@NotNull @NotNull String x, @NotNull @NotNull Function<Term,Term> body)

    • app

      @NotNull default @NotNull Term app(@NotNull @NotNull Term... args)

    • proj

      @NotNull default @NotNull Term proj(boolean isOne)

    • mkPi

      @NotNull static @NotNull Term mkPi(@NotNull @NotNull kala.collection.immutable.ImmutableSeq<Param<Term>> telescope, @NotNull @NotNull Term body)

    • mkPi

      @NotNull static @NotNull Term mkPi(@NotNull @NotNull Term dom, @NotNull @NotNull Term cod)

    • end

      @NotNull static @NotNull Term end(boolean isLeft)

    • neg

      @NotNull static @NotNull Term neg(@NotNull @NotNull Term term)

    • conn

      @NotNull static @NotNull Term conn(boolean isAnd, @NotNull @NotNull Term l, @NotNull @NotNull Term r)

    • and

      @NotNull static @NotNull Term and(@NotNull @NotNull Term l, @NotNull @NotNull Term r)

    • or

      @NotNull static @NotNull Term or(@NotNull @NotNull Term l, @NotNull @NotNull Term r)