# Metamath Zero logical model

While parsing a `.mm0` file, a Theory object is incrementally
constructed. A Theory object is characterized by the following
properties:

 * `sorts` (collection of Sort objects with different names)
 * `vars` (collection of Var objects with different names)
 * `terms` (collection of Term objects with different names)

## Sort object

A Sort object is characterized by the following properties:

 * `name` (identifier)
 * `pure` (boolean)
 * `strict` (boolean)
 * `provable` (boolean)
 * `nonempty` (boolean)

## Type object

A Type objects is characterized by the following properties:

 * `sort` (identifier which appears as `name` of a previously defined Sort object)
 * `dep_vars` (collection of identifiers which appear as `name` of previously defined Var objects)
 * `starred` (boolean, which must be false if `dep_bars` is non empty)

## Var object

A Var object is characterized by the following properties:

 * `name` (identifier)
 * `type` (a Type object)

## Term object

A Term object is characterized by the following properties:

 * `name` (identifier)
 * `in_types` (list of Type objects)
 * `out_type` (a Type object)