VarCat

computation.spad line 417 [edit on github]

VarCat represents a variable in Lambda and Ski domains. Since we are working in terms of functions then a variable will be a function (possibly a constant function) a variable has a name represented by a String. If the Lambda or Ski calculus is typed then the variable will also have a type.

= : (%, %) -> Boolean

return true if equal, that is names are equal and if there is a type then they must also be equal

coerce : % -> OutputForm

from CoercibleTo(OutputForm)

getName : % -> String

returns the name of the variable.

getType : % -> ILogic

returns the type of the variable. This may be a compound type, for instance ["a","b"] represents a->b a function from type a to type b untyped implementations return []

parseVar : String -> %

construct a variable by parsing a string

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

construct a variable by parsing a string pin is index to string at start of parse pout is index to string at end of parse

toString : % -> String

returns the name and the type in string form.

var : String -> %

constructs variable with a name but no type.

var : (String, ILogic) -> %

constructs variable with a name and also a type.

CoercibleTo(OutputForm)