Typed

computation.spad line 568 [edit on github]

Typed represents an typed variable in Lambda and Ski domains, a variable has a name represented by a String and a type represented by intutionistic logic.

= : (%, %) -> Boolean

from VarCat

coerce : % -> OutputForm

from CoercibleTo(OutputForm)

getName : % -> String

from VarCat

getType : % -> ILogic

from VarCat

parseVar : String -> %

from VarCat

parseVarTerm : (String, NonNegativeInteger) -> Record(rft : %, pout : NonNegativeInteger)

from VarCat

toString : % -> String

from VarCat

var : String -> %

from VarCat

var : (String, ILogic) -> %

from VarCat

CoercibleTo(OutputForm)

VarCat