Types

A Type describes a property of a Term. Terms are multifaceted and can be described from a variety of perspectives. A Term can have multiple properties, so Terms can also have multiple Types.

Each Term is associated with a singular Type Expression. A Type Expression represents all properties of that term, structured in Conjunctive Normal Form (CNF). Conjunctive Normal Form is just a way of saying that all the Ands are at the top level, above the Ors.

Two Types can be attached to one Term.

a: Integer + Prime

One Type can imply another Type. When this happens there is an implicit expansion of the implication to enforce CNF.

type Aa: Bb;
a : Aa      //                Aa + Aa => Bb
            //rewrite as just Aa + Bb
a : Aa + Bb
Copyright Andrew Johnson, 2023.