程序包 org.aya.guest0x0.syntax
package org.aya.guest0x0.syntax
-
类说明BdryData<E extends org.aya.pretty.doc.Docile & org.aya.guest0x0.cubical.Restr.TermLike<E>>CompData<Expr extends org.aya.pretty.doc.Docile>Concrete syntax of global definitions.For (maybe mutually) recursive definitions, like types and functionsUse with extreme caution: the field
DefVar.corecan be assigned only once after the core is generated."Proper" cubical subtypesinS/outS, the introduction/elimination rules for the subtype relation