# Type Definitions¶

In TorXakis, the user can define data types using the TYPEDEF keyword.

TorXakis will generate equality, type checking, and accessors functions for the user defined data types.

## Syntax¶

 typeDefs “TYPEDEF” typeDef (“;” typeDef)* “ENDDEF” typeDef typeName “::=” neConstructorList neConstructorList constructor (“|” constructor)* constructor constructorName (“{” neFieldsList “}”)? neFieldsList fields (“;” fields)* fields neFieldNameList “::” typeName neFieldNameList fieldName (“,” fieldName )* typeName CapsId constructorName CapsId fieldname SmallId

## Semantics¶

Define data types.
A data type has a unique typeName.
A data type must contain one or more constructors.
A data type cannot contain constructors with the same constructorName.
A constructor can contain zero or more fields.
A data type cannot contain fields with the same fieldname.
Hence, a constructor cannot contain fields with the same fieldname,
and multiple constructors cannot contain a field with the same fieldname.
The typeName associated with fields refers to a data type: either a predefined data type or a user defined data type.
A data type is called recursive when one or more fields refer to itself.

## Examples¶

The statement

TYPEDEF Point ::= CPoint { x, y :: Int } ENDDEF


defines the data type Point as the Cartesian product of two integers. These integers are referred to as x and y.

The statement

TYPEDEF Conditional_Int ::=
CAbsent_Int
| CPresent_Int { value :: Int }
ENDDEF


defines the data type Conditional_Int as the union of the absence of a value and the presence of any integer value.

The statement

TYPEDEF List_Int ::=
CNil_Int
|  Cstr_Int { head :: Int; tail :: List_Int }  ENDDEF


defines the recursive data type List_Int as the union of the empty list and the list constructor: The Cartesian product of an integer referred to as head, and a List_Int referred to as tail.